awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x →
      ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
        ∀ (i : I),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
              t =
            x i
x : FamilyOfElements P (ofArrows X π)
hx : x.Compatible (R := ofArrows X π)
⊢ ∃! t : P.obj (op B), x.IsAmalgamation (R := ofArrows X π) t
have refine_2 : ∀ (t : P.obj (op B))
  (hA :
    ∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          t =
        x (π i) sorry)
  (ht :
    ∀ (y : (fun (X : Type w) ↦ X) (P.obj (op B))),
      (fun (t : (fun (X : Type w) ↦ X) (P.obj (op B))) ↦
            ∀ (i : I),
              (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                    (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                  t =
                x (π i) sorry)
          y →
        y = t),
  ∃! t : P.obj (op B), x.IsAmalgamation (R := ofArrows X π) t
Tactic: obtain ⟨t, hA, ht⟩ := h (fun i ↦ x (π i) (ofArrows.mk _))
      (fun i j Z gi gj ↦ hx gi gj (ofArrows.mk _) (ofArrows.mk _))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
⊢ IsSheafFor P (ofArrows X π) ↔ Function.Bijective (Arrows.toCompatible P π)
have rw : (∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x →
      ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
        ∀ (i : I),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
              t =
            x i) ↔
  Function.Bijective (Arrows.toCompatible P π)
Tactic: rw [isSheafFor_arrows_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x →
        ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              x i) ↔
    Function.Bijective (Arrows.toCompatible P π)
have refine_1 : ∀
  (h :
    ∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x →
        ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              x i)
  (x : Subtype (Arrows.Compatible P π)) (y : (i : I) → P.obj (op (X i))) (hy : Arrows.Compatible P π y),
  ∃ (a : P.obj (op B)), Arrows.toCompatible P π a = Subtype.mk (p := Arrows.Compatible P π) y hy
Tactic: refine ⟨fun h ↦ ⟨fun x₁ x₂ hx ↦
      (h _ (Arrows.toCompatible P π x₁).property).unique (fun _ ↦ rfl)
        (congr_fun (congr_arg Subtype.val hx.symm)),
      fun ⟨y, hy⟩ ↦ ?_⟩, fun h x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
refine_1 :
  ∀
    (h :
      ∀ (x : (i : I) → P.obj (op (X i))),
        Arrows.Compatible P π x →
          ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
            ∀ (i : I),
              (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                    (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                  t =
                x i)
    (x : Subtype (Arrows.Compatible P π)) (y : (i : I) → P.obj (op (X i))) (hy : Arrows.Compatible P π y),
    ∃ (a : P.obj (op B)), Arrows.toCompatible P π a = Subtype.mk (p := Arrows.Compatible P π) y hy
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x →
        ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              x i) ↔
    Function.Bijective (Arrows.toCompatible P π)
have refine_2 : ∀ (h : Function.Bijective (Arrows.toCompatible P π)) (x : (i : I) → P.obj (op (X i))) (hx : Arrows.Compatible P π x),
  ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
    ∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          t =
        x i
Tactic: refine ⟨fun h ↦ ⟨fun x₁ x₂ hx ↦
      (h _ (Arrows.toCompatible P π x₁).property).unique (fun _ ↦ rfl)
        (congr_fun (congr_arg Subtype.val hx.symm)),
      fun ⟨y, hy⟩ ↦ ?_⟩, fun h x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x →
      ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
        ∀ (i : I),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
              t =
            x i
x : Subtype (Arrows.Compatible P π)
y : (i : I) → P.obj (op (X i))
hy : Arrows.Compatible P π y
⊢ ∃ (a : P.obj (op B)), Arrows.toCompatible P π a = Subtype.mk (p := Arrows.Compatible P π) y hy
have refine_1 : ∀ (x : P.obj (op B))
  (hx :
    ∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          x =
        y i),
  (∀ (y_1 : (fun (X : Type w) ↦ X) (P.obj (op B))),
      (fun (t : (fun (X : Type w) ↦ X) (P.obj (op B))) ↦
            ∀ (i : I),
              (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                    (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                  t =
                y i)
          y_1 →
        y_1 = x) →
    ∃ (a : P.obj (op B)), Arrows.toCompatible P π a = Subtype.mk (p := Arrows.Compatible P π) y hy
Tactic: obtain ⟨x, hx, _⟩ := h y hy
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x →
      ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
        ∀ (i : I),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
              t =
            x i
x_1 : Subtype (Arrows.Compatible P π)
y : (i : I) → P.obj (op (X i))
hy : Arrows.Compatible P π y
x : P.obj (op B)
hx :
  ∀ (i : I),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
        x =
      y i
right :
  ∀ (y_1 : (fun (X : Type w) ↦ X) (P.obj (op B))),
    (fun (t : (fun (X : Type w) ↦ X) (P.obj (op B))) ↦
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              y i)
        y_1 →
      y_1 = x
⊢ Arrows.toCompatible P π x = Subtype.mk (p := Arrows.Compatible P π) y hy
have a : ∀ (x_2 : I),
  (↑(Arrows.toCompatible P π x) : (i : I) → P.obj (op (X i))) x_2 =
    (↑(Subtype.mk (p := Arrows.Compatible P π) y hy) : (i : I) → P.obj (op (X i))) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : Function.Bijective (Arrows.toCompatible P π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
⊢ ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
    ∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          t =
        x i
have refine_2 : ∀ (y : P.obj (op B)) (hy : Arrows.toCompatible P π y = Subtype.mk (p := Arrows.Compatible P π) x hx),
  ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
    ∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          t =
        x i
Tactic: obtain ⟨y, hy⟩ := h.2 ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : Function.Bijective (Arrows.toCompatible P π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
y : P.obj (op B)
hy : Arrows.toCompatible P π y = Subtype.mk (p := Arrows.Compatible P π) x hx
⊢ ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
    ∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          t =
        x i
have hy₁ : (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i))) =
  (↑(Subtype.mk (p := Arrows.Compatible P π) x hx) : (i : I) → P.obj (op (X i)))
Tactic: rw [Subtype.ext_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : Function.Bijective (Arrows.toCompatible P π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
y : P.obj (op B)
hy : (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i))) = x
⊢ ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
    ∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          t =
        x i
have refine_2 : ∀ (hx : Arrows.Compatible P π (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i)))),
  ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
    ∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          t =
        (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i))) i
Tactic: subst hy
Cleared hypotheses: x, hx, hy
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : Function.Bijective (Arrows.toCompatible P π)
y : P.obj (op B)
hx : Arrows.Compatible P π (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i)))
y' : (fun (X : Type w) ↦ X) (P.obj (op B))
hy' :
  (fun (t : (fun (X : Type w) ↦ X) (P.obj (op B))) ↦
      ∀ (i : I),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
            t =
          (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i))) i)
    y'
⊢ Arrows.toCompatible P π y' = Arrows.toCompatible P π y
have a : ∀ (x : I),
  (↑(Arrows.toCompatible P π y') : (i : I) → P.obj (op (X i))) x =
    (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i))) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ X
inst_1 : IsIso f
⊢ IsSheafFor P (Sieve.pullback f R).arrows ↔ IsSheafFor P R.arrows
have obtain : ∀ (ι : Type (max u₁ v₁)) (Z : ι → C) (g : (i : ι) → Z i ⟶ X),
  IsSheafFor P (Sieve.pullback f (Sieve.ofArrows Z g)).arrows ↔ IsSheafFor P (Sieve.ofArrows Z g).arrows
Tactic: obtain ⟨ι, Z, g, rfl⟩ := R.exists_eq_ofArrows
Cleared hypotheses: R
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
⊢ IsSheafFor P (Sieve.pullback f (Sieve.ofArrows Z g)).arrows ↔ IsSheafFor P (Sieve.ofArrows Z g).arrows
have this : Sieve.pullback (asIso f).hom (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ (asIso f).inv
Tactic: have := Sieve.pullback_ofArrows_of_iso _ g (asIso f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
s : Subtype (Arrows.Compatible P g)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : Eq (α := W ⟶ Y) (g₁ ≫ (fun (i : ι) ↦ g i ≫ inv f) i₁) (g₂ ≫ (fun (i : ι) ↦ g i ≫ inv f) i₂)
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (Z i₁)))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
        ((fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) i₁) :
      (fun (X : Type w) ↦ X) (P.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (Z i₂)))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
        ((fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) i₂) :
      (fun (X : Type w) ↦ X) (P.obj (op W)))
have h₁ : g₁ ≫ g i₁ = g₂ ≫ g i₂
Tactic: simp only [← cancel_mono f, assoc, IsIso.inv_hom_id, comp_id] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
s : Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : g₁ ≫ g i₁ = g₂ ≫ g i₂
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (Z i₁)))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
        ((fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) i₁) :
      (fun (X : Type w) ↦ X) (P.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (Z i₂)))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
        ((fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) i₂) :
      (fun (X : Type w) ↦ X) (P.obj (op W)))
have h₁ : (g₁ ≫ g i₁) ≫ inv f = (g₂ ≫ g i₂) ≫ inv f
Tactic: replace h := h =≫ inv f
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
s : Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : (g₁ ≫ g i₁) ≫ inv f = (g₂ ≫ g i₂) ≫ inv f
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (Z i₁)))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
        ((fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) i₁) :
      (fun (X : Type w) ↦ X) (P.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (Z i₂)))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
        ((fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) i₂) :
      (fun (X : Type w) ↦ X) (P.obj (op W)))
have h₁ : g₁ ≫ g i₁ ≫ inv f = g₂ ≫ g i₂ ≫ inv f
Tactic: simp only [Category.assoc] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
e : Subtype (Arrows.Compatible P g) ≃
  Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f) :=
  {
    toFun := fun (s : Subtype (Arrows.Compatible P g)) ↦
      Subtype.mk (p := Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)
        (fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) ⋯,
    invFun :=
      fun (s : Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)) ↦
      Subtype.mk (p := Arrows.Compatible P g) (fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
⊢ IsSheafFor P (Sieve.pullback f (Sieve.ofArrows Z g)).arrows ↔ IsSheafFor P (Sieve.ofArrows Z g).arrows
have simp : Function.Bijective (α := P.obj (op Y)) (β :=
    Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f))
    (Arrows.toCompatible P fun (i : ι) ↦ g i ≫ inv f) ↔
  Function.Bijective (α := P.obj (op Y)) (β :=
    Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f))
    (((⇑e : (a : Subtype (Arrows.Compatible P g)) → Subtype (Arrows.Compatible P fun (i : ι) ↦ g i ≫ inv f)) ∘
        Arrows.toCompatible P g) ∘
      (⇑(P.mapIso (asIso f).symm.op).toEquiv : (a : P.obj (op Y)) → P.obj (op X)))
Tactic: simp only [this, ← isSheafFor_iff_generate,
    isSheafFor_ofArrows_iff_bijective_toCompabible, ← e.bijective.of_comp_iff',
    ← Function.Bijective.of_comp_iff _ (P.mapIso (asIso f).symm.op).toEquiv.bijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
e : Subtype (Arrows.Compatible P g) ≃
  Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f) :=
  {
    toFun := fun (s : Subtype (Arrows.Compatible P g)) ↦
      Subtype.mk (p := Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)
        (fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) ⋯,
    invFun :=
      fun (s : Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)) ↦
      Subtype.mk (p := Arrows.Compatible P g) (fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
⊢ Function.Bijective (α := P.obj (op Y)) (β :=
      Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f))
      (Arrows.toCompatible P fun (i : ι) ↦ g i ≫ inv f) ↔
    Function.Bijective (α := P.obj (op Y)) (β :=
      Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f))
      (((⇑e : (a : Subtype (Arrows.Compatible P g)) → Subtype (Arrows.Compatible P fun (i : ι) ↦ g i ≫ inv f)) ∘
          Arrows.toCompatible P g) ∘
        (⇑(P.mapIso (asIso f).symm.op).toEquiv : (a : P.obj (op Y)) → P.obj (op X)))
have h : Eq (α :=
  P.obj (op Y) → Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f))
  (((⇑e : (a : Subtype (Arrows.Compatible P g)) → Subtype (Arrows.Compatible P fun (i : ι) ↦ g i ≫ inv f)) ∘
      Arrows.toCompatible P g) ∘
    (⇑(P.mapIso (asIso f).symm.op).toEquiv : (a : P.obj (op Y)) → P.obj (op X)))
  (Arrows.toCompatible P fun (i : ι) ↦ g i ≫ inv f)
Tactic: convert! Iff.rfl using 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
e : Subtype (Arrows.Compatible P g) ≃
  Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f) :=
  {
    toFun := fun (s : Subtype (Arrows.Compatible P g)) ↦
      Subtype.mk (p := Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)
        (fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) ⋯,
    invFun :=
      fun (s : Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)) ↦
      Subtype.mk (p := Arrows.Compatible P g) (fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
⊢ Eq (α :=
    P.obj (op Y) → Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f))
    (((⇑e : (a : Subtype (Arrows.Compatible P g)) → Subtype (Arrows.Compatible P fun (i : ι) ↦ g i ≫ inv f)) ∘
        Arrows.toCompatible P g) ∘
      (⇑(P.mapIso (asIso f).symm.op).toEquiv : (a : P.obj (op Y)) → P.obj (op X)))
    (Arrows.toCompatible P fun (i : ι) ↦ g i ≫ inv f)
have h : ∀ (x : P.obj (op Y)) (x_1 : ι),
  Eq.{w + 1} (α := P.obj (op (Z x_1)))
    ((↑((((⇑e : (a : Subtype (Arrows.Compatible P g)) → Subtype (Arrows.Compatible P fun (i : ι) ↦ g i ≫ inv f)) ∘
                  Arrows.toCompatible P g) ∘
                (⇑(P.mapIso (asIso f).symm.op).toEquiv : (a : P.obj (op Y)) → P.obj (op X)))
              x) :
          (i : ι) → P.obj (op (Z i)))
        x_1 :
      P.obj (op (Z x_1)))
    ((↑(Arrows.toCompatible P (fun (i : ι) ↦ g i ≫ inv f) x) : (i : ι) → P.obj (op (Z i))) x_1 : P.obj (op (Z x_1)))
Tactic: ext