awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
⊢ Sieve.pullback ψ (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))) ∈
    (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) R
have h : Membership.mem (γ := Set (Sieve.{v_1, u_1} (C := C) (sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i)))
  ((Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a))
    (sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i))
  (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)))
Tactic: apply pullback_stable
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
Q E : C
e : Q ⟶ E
r : E ⟶ sigmaObj.{0, v_1, u_1} X
hq : Presieve.ofArrows X (fun (i : I) ↦ Sigma.ι X i) r
⊢ Presieve.ofArrows X f (r ≫ Sigma.desc f)
have mk : ∀ (i : I) (e : Q ⟶ X i),
  Presieve.ofArrows X f (CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} X) (Sigma.ι X i) (Sigma.desc f))
Tactic: cases hq
Cleared hypotheses: E, e, r, hq
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} (C := C) (sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i)))
    ((Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a))
      (sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i))
    (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)))
have this : LE.le (α := Sieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} X)) (generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i))
  (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)))
Tactic: have : generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i) ≤
            (generate (Presieve.ofArrows X f)).pullback (Sigma.desc f) := by
          rintro Q q ⟨E, e, r, ⟨hq, rfl⟩⟩
          exact ⟨E, e, r ≫ (Sigma.desc f), by cases hq; simpa using Presieve.ofArrows.mk _, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
this :
  LE.le (α := Sieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} X)) (generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i))
    (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)))
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} (C := C) (sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i)))
    ((Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a))
      (sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i))
    (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)))
have h : Coverage.Saturate.{v_1, u_1} (extensiveCoverage C ⊔ regularCoverage C) (sigmaObj.{0, v_1, u_1} X)
  (generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i))
Tactic: apply Coverage.saturate_of_superset _ this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
this :
  LE.le (α := Sieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} X)) (generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i))
    (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)))
⊢ Coverage.Saturate.{v_1, u_1} (extensiveCoverage C ⊔ regularCoverage C) (sigmaObj.{0, v_1, u_1} X)
    (generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i))
have h : Membership.mem (γ := Set (Presieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} X)))
  (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C ⊔ regularCoverage C)) (sigmaObj.{0, v_1, u_1} X))
  (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i)
Tactic: apply Coverage.Saturate.of
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
this :
  LE.le (α := Sieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} X)) (generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i))
    (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)))
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} X)))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C ⊔ regularCoverage C))
      (sigmaObj.{0, v_1, u_1} X))
    (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i)
have h : IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} X) (Y := sigmaObj.{0, v_1, u_1} X)
  (Sigma.desc fun (i : I) ↦ Sigma.ι X i)
Tactic: refine Or.inl ⟨I, inferInstance, _, _, ⟨rfl, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
this :
  LE.le (α := Sieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} X)) (generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i))
    (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)))
⊢ IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} X) (Y := sigmaObj.{0, v_1, u_1} X)
    (Sigma.desc fun (i : I) ↦ Sigma.ι X i)
have h : sigmaObj.{0, v_1, u_1} X = sigmaObj.{0, v_1, u_1} X →
  (Sigma.desc fun (i : I) ↦ Sigma.ι X i) = 𝟙 (sigmaObj.{0, v_1, u_1} X)
Tactic: convert! IsIso.id _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y : C
T S_1 : Sieve.{v_1, u_1} Y
h : Coverage.Saturate (coherentCoverage C) Y T
h_1 : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S_1)
a_ih : T ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
a_ih_1 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Sieve.pullback f S_1 ∈
        (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y_1
⊢ S_1 ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
have h : Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y T
Tactic: apply Coverage.Saturate.transitive Y T
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y : C
T S_1 : Sieve.{v_1, u_1} Y
h_1 : Coverage.Saturate (coherentCoverage C) Y T
h_2 : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S_1)
a_ih : T ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
a_ih_1 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Sieve.pullback f S_1 ∈
        (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y_1
h : Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y T
⊢ S_1 ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
have h₁ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
  T.arrows f → Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1 (Sieve.pullback f S_1)
Tactic: apply Coverage.Saturate.transitive Y T
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y : C
T S_1 : Sieve.{v_1, u_1} Y
h : Coverage.Saturate (coherentCoverage C) Y T
h_1 : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S_1)
a_ih : T ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
a_ih_1 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Sieve.pullback f S_1 ∈
        (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y_1
⊢ S_1 ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
have h : Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y T
Tactic: apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y : C
T S_1 : Sieve.{v_1, u_1} Y
h_1 : Coverage.Saturate (coherentCoverage C) Y T
h_2 : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S_1)
a_ih : T ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
a_ih_1 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Sieve.pullback f S_1 ∈
        (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y_1
h : Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y T
⊢ S_1 ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
have h₁ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
  T.arrows f → Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1 (Sieve.pullback f S_1)
Tactic: apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
h : S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B
⊢ S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B
have h₁ : ∀ (Y : C) (T : Presieve.{v_1, u_1} Y)
  (hT :
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
      (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) Y) T),
  generate T ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
Tactic: induction h with
    | of Y T hT =>
      obtain ⟨I, _, X, f, rfl, hT⟩ := hT
      apply Coverage.Saturate.transitive Y (generate (Presieve.ofArrows
        (fun (_ : Unit) ↦ (∐ fun (i : I) => X i)) (fun (_ : Unit) ↦ Sigma.desc f)))
      · apply Coverage.Saturate.of
        simp only [Coverage.sup_covering, extensiveCoverage, regularCoverage, Set.mem_union,
          Set.mem_setOf_eq]
        exact Or.inr ⟨_, Sigma.desc f, ⟨rfl, inferInstance⟩⟩
      · rintro R g ⟨W, ψ, σ, ⟨⟩, rfl⟩
        change _ ∈ ((extensiveCoverage C) ⊔ (regularCoverage C)).toGrothendieck R
        rw [Sieve.pullback_comp]
        apply pullback_stable
        have : generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i) ≤
            (generate (Presieve.ofArrows X f)).pullback (Sigma.desc f) := by
          rintro Q q ⟨E, e, r, ⟨hq, rfl⟩⟩
          exact ⟨E, e, r ≫ (Sigma.desc f), by cases hq; simpa using Presieve.ofArrows.mk _, by simp⟩
        apply Coverage.saturate_of_superset _ this
        apply Coverage.Saturate.of
        refine Or.inl ⟨I, inferInstance, _, _, ⟨rfl, ?_⟩⟩
        convert! IsIso.id _
        aesop
    | top => apply Coverage.Saturate.top
    | transitive Y T => apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
h : S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B
h₁ :
  ∀ (Y : C) (T : Presieve.{v_1, u_1} Y)
    (hT :
      Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) Y) T),
    generate T ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
⊢ S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B
have h₂ : ∀ (X : C), ⊤ ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) X
Tactic: induction h with
    | of Y T hT =>
      obtain ⟨I, _, X, f, rfl, hT⟩ := hT
      apply Coverage.Saturate.transitive Y (generate (Presieve.ofArrows
        (fun (_ : Unit) ↦ (∐ fun (i : I) => X i)) (fun (_ : Unit) ↦ Sigma.desc f)))
      · apply Coverage.Saturate.of
        simp only [Coverage.sup_covering, extensiveCoverage, regularCoverage, Set.mem_union,
          Set.mem_setOf_eq]
        exact Or.inr ⟨_, Sigma.desc f, ⟨rfl, inferInstance⟩⟩
      · rintro R g ⟨W, ψ, σ, ⟨⟩, rfl⟩
        change _ ∈ ((extensiveCoverage C) ⊔ (regularCoverage C)).toGrothendieck R
        rw [Sieve.pullback_comp]
        apply pullback_stable
        have : generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i) ≤
            (generate (Presieve.ofArrows X f)).pullback (Sigma.desc f) := by
          rintro Q q ⟨E, e, r, ⟨hq, rfl⟩⟩
          exact ⟨E, e, r ≫ (Sigma.desc f), by cases hq; simpa using Presieve.ofArrows.mk _, by simp⟩
        apply Coverage.saturate_of_superset _ this
        apply Coverage.Saturate.of
        refine Or.inl ⟨I, inferInstance, _, _, ⟨rfl, ?_⟩⟩
        convert! IsIso.id _
        aesop
    | top => apply Coverage.Saturate.top
    | transitive Y T => apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
h : S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B
h₁ :
  ∀ (Y : C) (T : Presieve.{v_1, u_1} Y)
    (hT :
      Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) Y) T),
    generate T ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
h₂ : ∀ (X : C), ⊤ ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) X
⊢ S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B
have h₃ : ∀ (Y : C) (T S : Sieve.{v_1, u_1} Y),
  Coverage.Saturate (coherentCoverage C) Y T →
    (∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)) →
      T ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y →
        (∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
            T.arrows f →
              Sieve.pullback f S ∈
                (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y_1) →
          S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
Tactic: induction h with
    | of Y T hT =>
      obtain ⟨I, _, X, f, rfl, hT⟩ := hT
      apply Coverage.Saturate.transitive Y (generate (Presieve.ofArrows
        (fun (_ : Unit) ↦ (∐ fun (i : I) => X i)) (fun (_ : Unit) ↦ Sigma.desc f)))
      · apply Coverage.Saturate.of
        simp only [Coverage.sup_covering, extensiveCoverage, regularCoverage, Set.mem_union,
          Set.mem_setOf_eq]
        exact Or.inr ⟨_, Sigma.desc f, ⟨rfl, inferInstance⟩⟩
      · rintro R g ⟨W, ψ, σ, ⟨⟩, rfl⟩
        change _ ∈ ((extensiveCoverage C) ⊔ (regularCoverage C)).toGrothendieck R
        rw [Sieve.pullback_comp]
        apply pullback_stable
        have : generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i) ≤
            (generate (Presieve.ofArrows X f)).pullback (Sigma.desc f) := by
          rintro Q q ⟨E, e, r, ⟨hq, rfl⟩⟩
          exact ⟨E, e, r ≫ (Sigma.desc f), by cases hq; simpa using Presieve.ofArrows.mk _, by simp⟩
        apply Coverage.saturate_of_superset _ this
        apply Coverage.Saturate.of
        refine Or.inl ⟨I, inferInstance, _, _, ⟨rfl, ?_⟩⟩
        convert! IsIso.id _
        aesop
    | top => apply Coverage.Saturate.top
    | transitive Y T => apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Equivalence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : Precoherent.{v_1, u_1} C
e : Equivalence.{v_1, v_2, u_1, u_2} C D
⊢ ∀ {X : D} {S : Sieve.{v_2, u_2} X},
    Membership.mem (γ := Set (Sieve.{v_1, u_1} (e.inverse.obj X)))
        ((coherentTopology C : (a : C) → Set (Sieve a)) (e.inverse.obj X)) (Sieve.functorPushforward e.inverse S) ↔
      S ∈ (coherentTopology D : (a : D) → Set (Sieve a)) X
have rw : ∀ {X : D} {S : Sieve.{v_2, u_2} X},
  Membership.mem (γ := Set (Sieve.{v_1, u_1} (e.inverse.obj X)))
      ((coherentTopology C : (a : C) → Set (Sieve a)) (e.inverse.obj X)) (Sieve.functorPushforward e.inverse S) ↔
    S ∈ (e.inverse.inducedTopology (coherentTopology C) : (a : D) → Set (Sieve a)) X
Tactic: rw [coherentTopology.eq_induced e.inverse]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Equivalence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : Precoherent.{v_1, u_1} C
A : Type u_3
inst_3 : Category.{v_3, u_3} A
e : Equivalence.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_3, u_1, u_3} Cᵒᵖ A
⊢ IsSheaf (coherentTopology C) F ↔ IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)
have refine : ∀ (hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)), IsSheaf (coherentTopology C) F
Tactic: refine ⟨fun hF ↦ ((e.sheafCongrPrecoherent A).functor.obj ⟨F, hF⟩).property, fun hF ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Equivalence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : Precoherent.{v_1, u_1} C
A : Type u_3
inst_3 : Category.{v_3, u_3} A
e : Equivalence.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_3, u_1, u_3} Cᵒᵖ A
hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)
⊢ IsSheaf (coherentTopology C) F
have rw : IsSheaf (coherentTopology C) (e.functor.op ⋙ e.inverse.op ⋙ F)
Tactic: rw [isSheaf_of_iso_iff (P' := e.functor.op ⋙ e.inverse.op ⋙ F)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Equivalence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : Precoherent.{v_1, u_1} C
A : Type u_3
inst_3 : Category.{v_3, u_3} A
e : Equivalence.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_3, u_1, u_3} Cᵒᵖ A
hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)
rw : IsSheaf (coherentTopology C) (e.functor.op ⋙ e.inverse.op ⋙ F)
⊢ IsSheaf (coherentTopology C) F
have rw₁ : F ≅ e.functor.op ⋙ e.inverse.op ⋙ F
Tactic: rw [isSheaf_of_iso_iff (P' := e.functor.op ⋙ e.inverse.op ⋙ F)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Equivalence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : Preregular.{v_1, u_1} C
e : Equivalence.{v_1, v_2, u_1, u_2} C D
⊢ ∀ {X : D} {S : Sieve.{v_2, u_2} X},
    Membership.mem (γ := Set (Sieve.{v_1, u_1} (e.inverse.obj X)))
        ((regularTopology C : (a : C) → Set (Sieve a)) (e.inverse.obj X)) (Sieve.functorPushforward e.inverse S) ↔
      S ∈ (regularTopology D : (a : D) → Set (Sieve a)) X
have rw : ∀ {X : D} {S : Sieve.{v_2, u_2} X},
  Membership.mem (γ := Set (Sieve.{v_1, u_1} (e.inverse.obj X)))
      ((regularTopology C : (a : C) → Set (Sieve a)) (e.inverse.obj X)) (Sieve.functorPushforward e.inverse S) ↔
    S ∈ (e.inverse.inducedTopology (regularTopology C) : (a : D) → Set (Sieve a)) X
Tactic: rw [regularTopology.eq_induced e.inverse]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Equivalence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : Preregular.{v_1, u_1} C
A : Type u_3
inst_3 : Category.{v_3, u_3} A
e : Equivalence.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_3, u_1, u_3} Cᵒᵖ A
⊢ IsSheaf (regularTopology C) F ↔ IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
have refine : ∀ (hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)), IsSheaf (regularTopology C) F
Tactic: refine ⟨fun hF ↦ ((e.sheafCongrPreregular A).functor.obj ⟨F, hF⟩).property, fun hF ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Equivalence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : Preregular.{v_1, u_1} C
A : Type u_3
inst_3 : Category.{v_3, u_3} A
e : Equivalence.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_3, u_1, u_3} Cᵒᵖ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
⊢ IsSheaf (regularTopology C) F
have rw : IsSheaf (regularTopology C) (e.functor.op ⋙ e.inverse.op ⋙ F)
Tactic: rw [isSheaf_of_iso_iff (P' := e.functor.op ⋙ e.inverse.op ⋙ F)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Equivalence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : Preregular.{v_1, u_1} C
A : Type u_3
inst_3 : Category.{v_3, u_3} A
e : Equivalence.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_3, u_1, u_3} Cᵒᵖ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
rw : IsSheaf (regularTopology C) (e.functor.op ⋙ e.inverse.op ⋙ F)
⊢ IsSheaf (regularTopology C) F
have rw₁ : F ≅ e.functor.op ⋙ e.inverse.op ⋙ F
Tactic: rw [isSheaf_of_iso_iff (P' := e.functor.op ⋙ e.inverse.op ⋙ F)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits (goal)
Goal:
A : Type u_1
C : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} J
inst_3 : FinitaryExtensive.{v_2, u_2} C
inst_4 : HasColimitsOfShape.{v_3, u_3, v_1, u_1} J A
inst_5 : PreservesFiniteProducts (C := Functor.{v_3, v_1, u_3, u_1} J A) colim
G : J ⥤ Sheaf.{v_2, v_1, u_2, u_1} (extensiveTopology C) A
⊢ Presheaf.IsSheaf (extensiveTopology C) (pointwiseCocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)).pt
have rw : PreservesFiniteProducts (pointwiseCocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)).pt
Tactic: rw [Presheaf.isSheaf_iff_preservesFiniteProducts]