awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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} (𝟙 (sigmaObj.{0, v_1, u_1} X))

Tactic:
IsIso.id _

Premises used: CategoryTheory.IsIso.id
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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)))
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)
⊢ 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:
convert! IsIso.id _

Premises used: CategoryTheory.IsIso.id
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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)))
e_4 : 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:
aesop
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
X : C
⊢ ⊤ ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) X

Tactic:
apply Coverage.Saturate.top

Premises used: CategoryTheory.Coverage.Saturate.top
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
h₁ :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1 (Sieve.pullback f S_1)
⊢ S_1 ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y

Tactic:
apply Coverage.Saturate.transitive Y T

Premises used: CategoryTheory.Coverage.Saturate.transitive
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
⊢ Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y T

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1 (Sieve.pullback f S_1)

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
h₁ :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1 (Sieve.pullback f S_1)
h₂ : Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y T
h₃ :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1 (Sieve.pullback f S_1)
⊢ S_1 ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y

Tactic:
apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]

Premises used: CategoryTheory.Coverage.Saturate.transitive
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
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
⊢ S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B

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]

Premises used: Set.mem_union, CategoryTheory.GrothendieckTopology.transitive, CategoryTheory.regularCoverage, CategoryTheory.Coverage.Saturate.top, CategoryTheory.GrothendieckTopology.pullback_stable, Set.mem_setOf_eq, CategoryTheory.Coverage.Saturate.of, CategoryTheory.extensiveCoverage, CategoryTheory.Sieve.pullback_comp, Or.inl, CategoryTheory.Coverage.sup_covering, Or.inr, CategoryTheory.IsIso.id, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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
⊢ Precoherent.{v_2, u_2} D

Tactic:
e.inverse.reflects_precoherent

Premises used: CategoryTheory.Functor.reflects_precoherent, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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
inst_3 : EssentiallySmall.{u_3, v_1, u_1} C
⊢ Precoherent.{u_3, u_3} (SmallModel.{u_3, v_1, u_1} C)

Tactic:
(equivSmallModel C).precoherent

Premises used: CategoryTheory.Equivalence.precoherent, CategoryTheory.equivSmallModel
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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
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
⊢ ∀ {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

Tactic:
rw [coherentTopology.eq_induced e.inverse]

Premises used: CategoryTheory.coherentTopology.eq_induced, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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 ∈ (e.inverse.inducedTopology (coherentTopology C) : (a : D) → Set (Sieve a)) X

Tactic:
simp only [Functor.mem_inducedTopology_sieves_iff, implies_true]

Premises used: implies_true, CategoryTheory.Functor.mem_inducedTopology_sieves_iff
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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)

Tactic:
⟨fun hF ↦ ((e.sheafCongrPrecoherent A).functor.obj ⟨F, hF⟩).property, fun hF ↦ ?_⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Equivalence.sheafCongrPrecoherent, CategoryTheory.Equivalence.functor, Iff.intro, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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
refine : ∀ (hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)), IsSheaf (coherentTopology C) F
⊢ IsSheaf (coherentTopology C) F ↔ IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)

Tactic:
refine ⟨fun hF ↦ ((e.sheafCongrPrecoherent A).functor.obj ⟨F, hF⟩).property, fun hF ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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)
rw₁ : F ≅ e.functor.op ⋙ e.inverse.op ⋙ F
⊢ IsSheaf (coherentTopology C) F

Tactic:
rw [isSheaf_of_iso_iff (P' := e.functor.op ⋙ e.inverse.op ⋙ F)]

Premises used: CategoryTheory.Presheaf.isSheaf_of_iso_iff
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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) (e.functor.op ⋙ e.inverse.op ⋙ F)

Tactic:
(e.sheafCongrPrecoherent A).inverse.obj ⟨e.inverse.op ⋙ F, hF⟩ |>.property

Premises used: CategoryTheory.Functor.op, CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Equivalence.sheafCongrPrecoherent, CategoryTheory.Functor.comp, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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) (e.functor.op ⋙ e.inverse.op ⋙ F)

Tactic:
exact (e.sheafCongrPrecoherent A).inverse.obj ⟨e.inverse.op ⋙ F, hF⟩ |>.property

Premises used: CategoryTheory.Functor.op, CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Equivalence.sheafCongrPrecoherent, CategoryTheory.Functor.comp, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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)
⊢ F ≅ e.functor.op ⋙ e.inverse.op ⋙ F

Tactic:
exact Functor.isoWhiskerRight e.op.unitIso F

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Equivalence.op, CategoryTheory.Functor.isoWhiskerRight
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
A : Type u_3
inst_2 : Category.{v_3, u_3} A
inst_3 : EssentiallySmall.{u_4, v_1, u_1} C
F : Functor.{v_1, v_3, u_1, u_3} Cᵒᵖ A
⊢ IsSheaf (coherentTopology C) F ↔
    IsSheaf.{u_4, v_3, u_4, u_3} (C := SmallModel.{u_4, v_1, u_1} C) (coherentTopology (SmallModel.{u_4, v_1, u_1} C))
      (Functor.op (inverse (equivSmallModel C)) ⋙ F)

Tactic:
precoherent_isSheaf_iff _ _ _

Premises used: CategoryTheory.Equivalence.precoherent_isSheaf_iff
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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
⊢ Preregular.{v_2, u_2} D

Tactic:
e.inverse.reflects_preregular

Premises used: CategoryTheory.Functor.reflects_preregular, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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
inst_3 : EssentiallySmall.{u_3, v_1, u_1} C
⊢ Preregular.{u_3, u_3} (SmallModel.{u_3, v_1, u_1} C)

Tactic:
(equivSmallModel C).preregular

Premises used: CategoryTheory.Equivalence.preregular, CategoryTheory.equivSmallModel
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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
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
⊢ ∀ {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

Tactic:
rw [regularTopology.eq_induced e.inverse]

Premises used: CategoryTheory.regularTopology.eq_induced, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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 ∈ (e.inverse.inducedTopology (regularTopology C) : (a : D) → Set (Sieve a)) X

Tactic:
simp only [Functor.mem_inducedTopology_sieves_iff, implies_true]

Premises used: implies_true, CategoryTheory.Functor.mem_inducedTopology_sieves_iff
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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)

Tactic:
⟨fun hF ↦ ((e.sheafCongrPreregular A).functor.obj ⟨F, hF⟩).property, fun hF ↦ ?_⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Equivalence.sheafCongrPreregular, CategoryTheory.Equivalence.functor, Iff.intro, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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
refine : ∀ (hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)), IsSheaf (regularTopology C) F
⊢ IsSheaf (regularTopology C) F ↔ IsSheaf (regularTopology D) (e.inverse.op ⋙ F)

Tactic:
refine ⟨fun hF ↦ ((e.sheafCongrPreregular A).functor.obj ⟨F, hF⟩).property, fun hF ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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)
rw₁ : F ≅ e.functor.op ⋙ e.inverse.op ⋙ F
⊢ IsSheaf (regularTopology C) F

Tactic:
rw [isSheaf_of_iso_iff (P' := e.functor.op ⋙ e.inverse.op ⋙ F)]

Premises used: CategoryTheory.Presheaf.isSheaf_of_iso_iff
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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) (e.functor.op ⋙ e.inverse.op ⋙ F)

Tactic:
(e.sheafCongrPreregular A).inverse.obj ⟨e.inverse.op ⋙ F, hF⟩ |>.property

Premises used: CategoryTheory.Functor.op, CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.comp, CategoryTheory.Equivalence.sheafCongrPreregular, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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) (e.functor.op ⋙ e.inverse.op ⋙ F)

Tactic:
exact (e.sheafCongrPreregular A).inverse.obj ⟨e.inverse.op ⋙ F, hF⟩ |>.property

Premises used: CategoryTheory.Functor.op, CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.comp, CategoryTheory.Equivalence.sheafCongrPreregular, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
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)
⊢ F ≅ e.functor.op ⋙ e.inverse.op ⋙ F

Tactic:
exact Functor.isoWhiskerRight e.op.unitIso F

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Equivalence.op, CategoryTheory.Functor.isoWhiskerRight
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
A : Type u_3
inst_2 : Category.{v_3, u_3} A
inst_3 : EssentiallySmall.{u_4, v_1, u_1} C
F : Functor.{v_1, v_3, u_1, u_3} Cᵒᵖ A
⊢ IsSheaf (regularTopology C) F ↔
    IsSheaf.{u_4, v_3, u_4, u_3} (C := SmallModel.{u_4, v_1, u_1} C) (regularTopology (SmallModel.{u_4, v_1, u_1} C))
      (Functor.op (inverse (equivSmallModel C)) ⋙ F)

Tactic:
preregular_isSheaf_iff _ _ _

Premises used: CategoryTheory.Equivalence.preregular_isSheaf_iff