awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X : C
S : Sieve.{u_1, u_2} X
hS : S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X
refine_1 :
  ∀ (X : C) (R : Presieve.{u_1, u_2} X) (hR : R ∈ J.coverings X), ∃ R_1 ∈ J.coverings X, R_1 ≤ (Sieve.generate R).arrows
refine_1₁ : ∀ (X : C), ∃ R ∈ J.coverings X, R ≤ Sieve.arrows ⊤
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows
have refine_1₂ : ∀ (X : C) (S : Sieve.{u_1, u_2} X) (hS : J.Saturate X S) (Y : C) (f : Y ⟶ X) (h : ∃ R ∈ J.coverings X, R ≤ S.arrows),
  ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows
Tactic: induction hS with
    | of X R hR =>
      use R, hR
      exact Sieve.le_generate R
    | top X =>
      exact ⟨Presieve.singleton (𝟙 X), mem_coverings_of_isIso (𝟙 X), by simp⟩
    | pullback X S hS Y f h =>
      obtain ⟨R, hR, hle⟩ := h
      have : R.HasPullbacks f := J.hasPullbacks_of_mem f hR
      refine ⟨R.pullbackArrows f, pullbackArrows_mem f hR, ?_⟩
      rw [← Sieve.generate_le_iff, Sieve.pullbackArrows_comm]
      apply Sieve.pullback_monotone
      rwa [Sieve.generate_le_iff]
    | transitive X S T hS hT hleS hleT =>
      obtain ⟨R, hR, hle⟩ := hleS
      rw [mem_iff_exists_zeroHypercover] at hR
      obtain ⟨E, rfl⟩ := hR
      replace hleT (i : E.I₀) : ∃ (F : J.ZeroHypercover (E.X i)),
          F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows := by
        obtain ⟨R', hR', hle'⟩ := hleT (hle _ _ ⟨i⟩)
        rw [mem_iff_exists_zeroHypercover] at hR'
        obtain ⟨F, rfl⟩ := hR'
        use F
      choose F hle' using hleT
      refine ⟨(E.bind F).presieve₀, (E.bind F).mem₀, ?_⟩
      rw [Presieve.ofArrows_le_iff]
      intro i
      exact hle' _ _ _ ⟨i.snd⟩
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X : C
S : Sieve.{u_1, u_2} X
hS : S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X
refine_1 :
  ∀ (X : C) (R : Presieve.{u_1, u_2} X) (hR : R ∈ J.coverings X), ∃ R_1 ∈ J.coverings X, R_1 ≤ (Sieve.generate R).arrows
refine_1₁ : ∀ (X : C), ∃ R ∈ J.coverings X, R ≤ Sieve.arrows ⊤
refine_1₂ :
  ∀ (X : C) (S : Sieve.{u_1, u_2} X) (hS : J.Saturate X S) (Y : C) (f : Y ⟶ X) (h : ∃ R ∈ J.coverings X, R ≤ S.arrows),
    ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows
have refine_1₃ : ∀ (X : C) (S T : Sieve.{u_1, u_2} X) (hS : J.Saturate X S)
  (hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T))
  (hleS : ∃ R ∈ J.coverings X, R ≤ S.arrows)
  (hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows),
  ∃ R ∈ J.coverings X, R ≤ T.arrows
Tactic: induction hS with
    | of X R hR =>
      use R, hR
      exact Sieve.le_generate R
    | top X =>
      exact ⟨Presieve.singleton (𝟙 X), mem_coverings_of_isIso (𝟙 X), by simp⟩
    | pullback X S hS Y f h =>
      obtain ⟨R, hR, hle⟩ := h
      have : R.HasPullbacks f := J.hasPullbacks_of_mem f hR
      refine ⟨R.pullbackArrows f, pullbackArrows_mem f hR, ?_⟩
      rw [← Sieve.generate_le_iff, Sieve.pullbackArrows_comm]
      apply Sieve.pullback_monotone
      rwa [Sieve.generate_le_iff]
    | transitive X S T hS hT hleS hleT =>
      obtain ⟨R, hR, hle⟩ := hleS
      rw [mem_iff_exists_zeroHypercover] at hR
      obtain ⟨E, rfl⟩ := hR
      replace hleT (i : E.I₀) : ∃ (F : J.ZeroHypercover (E.X i)),
          F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows := by
        obtain ⟨R', hR', hle'⟩ := hleT (hle _ _ ⟨i⟩)
        rw [mem_iff_exists_zeroHypercover] at hR'
        obtain ⟨F, rfl⟩ := hR'
        use F
      choose F hle' using hleT
      refine ⟨(E.bind F).presieve₀, (E.bind F).mem₀, ?_⟩
      rw [Presieve.ofArrows_le_iff]
      intro i
      exact hle' _ _ _ ⟨i.snd⟩
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (hypothesis)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X : C
S : Sieve.{u_1, u_2} X
h : ∃ R ∈ J.coverings X, R ≤ S.arrows
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
⊢ S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X
have hle₁ : Sieve.generate R ≤ S
Tactic: rw [← Sieve.generate_le_iff] at hle
Cleared hypotheses: hle
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X : C
S : Sieve.{u_1, u_2} X
h : ∃ R ∈ J.coverings X, R ≤ S.arrows
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : Sieve.generate R ≤ S
⊢ S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X
have refine_2 : Sieve.generate R ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X
Tactic: apply GrothendieckTopology.superset_covering _ hle
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : Limits.HasPullbacks.{u_1, u_2} C
inst_4 : J.HasIsos
⊢ Pretopology.toGrothendieck (toPretopology C J) = J.toGrothendieck
have h : ∀ (x : C) (x_1 : Sieve.{u_1, u_2} x),
  x_1 ∈ (Pretopology.toGrothendieck (toPretopology C J) : (a : C) → Set (Sieve a)) x ↔
    x_1 ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
h : IsSheaf J.toGrothendieck P
S : C
R : Presieve.{u_2, u_3} S
hR : R ∈ J.coverings S
⊢ IsSheafFor P R
have rw : ∀ (h : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows) {S : C}
  {R : Presieve.{u_2, u_3} S} (hR : R ∈ J.coverings S), IsSheafFor P R
Tactic: rw [J.isSheaf_toGrothendieck_iff] at h
Cleared hypotheses: h, S, R, hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
F : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
S : C
𝒰 𝒱 : PreZeroHypercover.{u_4, u_2, u_3} S
e : 𝒰 ≅ 𝒱
⊢ Presieve.IsSheafFor F 𝒰.presieve₀ ↔ Presieve.IsSheafFor F 𝒱.presieve₀
have rw : Presieve.IsSheafFor F (Sieve.generate 𝒰.presieve₀).arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
Tactic: rw [Presieve.isSheafFor_iff_generate, ← Sieve.ofArrows, ← PreZeroHypercover.sieve₀,
    PreZeroHypercover.sieve₀_eq_of_iso e, ← Presieve.isSheafFor_iff_generate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
F : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
S : C
𝒰 𝒱 : PreZeroHypercover.{u_4, u_2, u_3} S
e : 𝒰 ≅ 𝒱
rw : Presieve.IsSheafFor F (Sieve.generate 𝒰.presieve₀).arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
⊢ Presieve.IsSheafFor F 𝒰.presieve₀ ↔ Presieve.IsSheafFor F 𝒱.presieve₀
have rw₁ : Presieve.IsSheafFor F (Sieve.ofArrows 𝒰.X 𝒰.f).arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
Tactic: rw [Presieve.isSheafFor_iff_generate, ← Sieve.ofArrows, ← PreZeroHypercover.sieve₀,
    PreZeroHypercover.sieve₀_eq_of_iso e, ← Presieve.isSheafFor_iff_generate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
F : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
S : C
𝒰 𝒱 : PreZeroHypercover.{u_4, u_2, u_3} S
e : 𝒰 ≅ 𝒱
rw : Presieve.IsSheafFor F (Sieve.generate 𝒰.presieve₀).arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
rw₁ : Presieve.IsSheafFor F (Sieve.ofArrows 𝒰.X 𝒰.f).arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
⊢ Presieve.IsSheafFor F 𝒰.presieve₀ ↔ Presieve.IsSheafFor F 𝒱.presieve₀
have rw₂ : Presieve.IsSheafFor F 𝒰.sieve₀.arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
Tactic: rw [Presieve.isSheafFor_iff_generate, ← Sieve.ofArrows, ← PreZeroHypercover.sieve₀,
    PreZeroHypercover.sieve₀_eq_of_iso e, ← Presieve.isSheafFor_iff_generate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
F : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
S : C
𝒰 𝒱 : PreZeroHypercover.{u_4, u_2, u_3} S
e : 𝒰 ≅ 𝒱
rw : Presieve.IsSheafFor F (Sieve.generate 𝒰.presieve₀).arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
rw₁ : Presieve.IsSheafFor F (Sieve.ofArrows 𝒰.X 𝒰.f).arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
rw₂ : Presieve.IsSheafFor F 𝒰.sieve₀.arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
⊢ Presieve.IsSheafFor F 𝒰.presieve₀ ↔ Presieve.IsSheafFor F 𝒱.presieve₀
have rw₃ : Presieve.IsSheafFor F 𝒱.sieve₀.arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
Tactic: rw [Presieve.isSheafFor_iff_generate, ← Sieve.ofArrows, ← PreZeroHypercover.sieve₀,
    PreZeroHypercover.sieve₀_eq_of_iso e, ← Presieve.isSheafFor_iff_generate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
F : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
S : C
𝒰 𝒱 : PreZeroHypercover.{u_4, u_2, u_3} S
e : 𝒰 ≅ 𝒱
rw : Presieve.IsSheafFor F (Sieve.generate 𝒰.presieve₀).arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
rw₁ : Presieve.IsSheafFor F (Sieve.ofArrows 𝒰.X 𝒰.f).arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
rw₂ : Presieve.IsSheafFor F 𝒰.sieve₀.arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
rw₃ : Presieve.IsSheafFor F 𝒱.sieve₀.arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
⊢ Presieve.IsSheafFor F 𝒰.presieve₀ ↔ Presieve.IsSheafFor F 𝒱.presieve₀
have rw₄ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒱.X 𝒱.f) ↔ Presieve.IsSheafFor F 𝒱.presieve₀
Tactic: rw [Presieve.isSheafFor_iff_generate, ← Sieve.ofArrows, ← PreZeroHypercover.sieve₀,
    PreZeroHypercover.sieve₀_eq_of_iso e, ← Presieve.isSheafFor_iff_generate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
F : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
S X Y : C
f : X ⟶ S
g : Y ⟶ S
e : X ≅ Y
he : e.hom ≫ g = f
⊢ IsSheafFor F (singleton f) ↔ IsSheafFor F (singleton g)
have subst : IsSheafFor F (singleton (e.hom ≫ g)) ↔ IsSheafFor F (singleton g)
Tactic: subst he
Cleared hypotheses: f, he
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
F : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
S X Y : C
g : Y ⟶ S
e : X ≅ Y
⊢ IsSheafFor F (singleton (e.hom ≫ g)) ↔ IsSheafFor F (singleton g)
have rw : IsSheafFor (X := S) F (ofArrows (fun (x : PUnit.{1}) ↦ X) fun (x : PUnit.{1}) ↦ e.hom ≫ g) ↔ IsSheafFor F (singleton g)
Tactic: rw [← Presieve.ofArrows_pUnit.{_, _, 0}, ← Presieve.ofArrows_pUnit,
    Presieve.isSheafFor_ofArrows_comp_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
F : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
S X Y : C
g : Y ⟶ S
e : X ≅ Y
rw :
  IsSheafFor (X := S) F (ofArrows (fun (x : PUnit.{1}) ↦ X) fun (x : PUnit.{1}) ↦ e.hom ≫ g) ↔
    IsSheafFor F (singleton g)
⊢ IsSheafFor F (singleton (e.hom ≫ g)) ↔ IsSheafFor F (singleton g)
have rw₁ : IsSheafFor (X := S) F (ofArrows (fun (x : PUnit.{1}) ↦ X) fun (x : PUnit.{1}) ↦ e.hom ≫ g) ↔
  IsSheafFor (X := S) F (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ g)
Tactic: rw [← Presieve.ofArrows_pUnit.{_, _, 0}, ← Presieve.ofArrows_pUnit,
    Presieve.isSheafFor_ofArrows_comp_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
F : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
S X Y : C
g : Y ⟶ S
e : X ≅ Y
rw :
  IsSheafFor (X := S) F (ofArrows (fun (x : PUnit.{1}) ↦ X) fun (x : PUnit.{1}) ↦ e.hom ≫ g) ↔
    IsSheafFor F (singleton g)
rw₁ :
  IsSheafFor (X := S) F (ofArrows (fun (x : PUnit.{1}) ↦ X) fun (x : PUnit.{1}) ↦ e.hom ≫ g) ↔
    IsSheafFor (X := S) F (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ g)
⊢ IsSheafFor F (singleton (e.hom ≫ g)) ↔ IsSheafFor F (singleton g)
have rw₂ : IsSheafFor (X := S) F (ofArrows (fun (i : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ g) ↔
  IsSheafFor (X := S) F (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ g)
Tactic: rw [← Presieve.ofArrows_pUnit.{_, _, 0}, ← Presieve.ofArrows_pUnit,
    Presieve.isSheafFor_ofArrows_comp_iff]
-- 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
R : Presieve.{u_3, u_4} X
inst_2 : R.HasPairwisePullbacks
inst_3 : F.PreservesPairwisePullbacks R
⊢ IsSheafFor (F.op ⋙ P) R ↔ IsSheafFor P (map F R)
have this : (map F R).HasPairwisePullbacks
Tactic: have : (R.map F).HasPairwisePullbacks := .map_of_preservesPairwisePullbacks _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
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
R : Presieve.{u_3, u_4} X
inst_2 : R.HasPairwisePullbacks
inst_3 : F.PreservesPairwisePullbacks R
this : (map F R).HasPairwisePullbacks
⊢ IsSheafFor (F.op ⋙ P) R ↔ IsSheafFor P (map F R)
have obtain : ∀ (ι : Type (max u_4 u_3)) (Y : ι → C) (f : (i : ι) → Y i ⟶ X) [(ofArrows Y f).HasPairwisePullbacks]
  [F.PreservesPairwisePullbacks (ofArrows Y f)] (this : (map F (ofArrows Y f)).HasPairwisePullbacks),
  IsSheafFor (F.op ⋙ P) (ofArrows Y f) ↔ IsSheafFor P (map F (ofArrows Y f))
Tactic: obtain ⟨ι, Y, f, rfl⟩ := R.exists_eq_ofArrows
Cleared hypotheses: R, inst_2, inst_3, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
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 : (map F (ofArrows Y f)).HasPairwisePullbacks
⊢ IsSheafFor (F.op ⋙ P) (ofArrows Y f) ↔ IsSheafFor P (map F (ofArrows Y f))
have rw : ∀
  (this :
    HasPairwisePullbacks.{v_1, u_1} (C := D) (X := F.obj X)
      (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))),
  IsSheafFor (F.op ⋙ P) (ofArrows Y f) ↔
    IsSheafFor (X := F.obj X) P (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
Tactic: rw [map_ofArrows] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
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 :
  HasPairwisePullbacks.{v_1, u_1} (C := D) (X := F.obj X)
    (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
⊢ IsSheafFor (F.op ⋙ P) (ofArrows Y f) ↔
    IsSheafFor (X := F.obj X) P (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
have simp_rw : (∀ (x : (i : ι) → (F.op ⋙ P).obj (Opposite.op (Y i))),
    Arrows.PullbackCompatible (F.op ⋙ P) f x →
      ∃! t : (F.op ⋙ P).obj (Opposite.op X),
        ∀ (i : ι),
          (ConcreteCategory.hom (FC := TypeCat.Fun) ((F.op ⋙ P).map (f i).op) :
                (a : (F.op ⋙ P).obj (Opposite.op X)) → (F.op ⋙ P).obj (Opposite.op (Y i)))
              t =
            x i) ↔
  ∀ (x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))),
    Arrows.PullbackCompatible P (B := F.obj X) (fun (i : ι) ↦ F.map (f i)) x →
      ∃! t : P.obj (Opposite.op (F.obj X)),
        ∀ (i : ι),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (F.map (f i)).op) :
                (a : P.obj (Opposite.op (F.obj X))) → P.obj (Opposite.op (F.obj (Y i))))
              t =
            x i
Tactic: simp_rw [Presieve.isSheafFor_arrows_iff_pullbacks]
-- 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 :
  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 : ι
⊢ Eq (α := P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (F.map (pullback.fst (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) (P.map (Quiver.Hom.op (F.map (pullback.snd (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₁ : PreservesLimit (cospan (f i) (f j)) F
Tactic: have : PreservesLimit (cospan (f i) (f j)) F :=
    F.preservesLimit_cospan_of_mem_presieve (ofArrows _ f) ⟨i⟩ ⟨j⟩
-- 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 : PreservesLimit (cospan (f i) (f j)) F
⊢ Eq (α := P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (F.map (pullback.fst (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) (P.map (Quiver.Hom.op (F.map (pullback.snd (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₁ : HasPullback (F.map (f i)) (F.map (f j))
Tactic: have : HasPullback (F.map (f i)) (F.map (f j)) := hasPullback_of_preservesPullback _ _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
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))
⊢ 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))))))
have rw : IsIso (X := P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j))))) (Y :=
  P.obj (Opposite.op (F.obj (pullback (f i) (f j))))) (P.map (Quiver.Hom.op (pullbackComparison F (f i) (f j))))
Tactic: rw [← isIso_iff_bijective]