awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} Cᵒᵖ (Type u_1)
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
x : F.obj (op X)
H :
  Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.fst.op) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
        x :
      (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.snd.op) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
        x :
      (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
Z : C
p₁ p₂ : Z ⟶ X
h : p₁ ≫ f = p₂ ≫ f
rw :
  Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (PullbackCone.IsLimit.lift hc p₁ p₂ h).op) :
          (a : F.obj (op c.pt)) → F.obj (op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.snd.op) :
              (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
            x :
          (fun (X : Type u_1) ↦ X) (F.obj (op c.pt))) :
      F.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₂.op) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
        x :
      (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₁.op) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
        x :
      (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₂.op) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
        x :
      (fun (X : Type u_1) ↦ X) (F.obj (op Z)))

Tactic:
rw [← PullbackCone.IsLimit.lift_fst hc _ _ h, op_comp, Functor.map_comp, comp_apply, H]

Premises used: CategoryTheory.op_comp, CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} Cᵒᵖ (Type u_1)
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
x : F.obj (op X)
H :
  Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.fst.op) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
        x :
      (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.snd.op) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
        x :
      (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
Z : C
p₁ p₂ : Z ⟶ X
h : p₁ ≫ f = p₂ ≫ f
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (PullbackCone.IsLimit.lift hc p₁ p₂ h).op) :
          (a : F.obj (op c.pt)) → F.obj (op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.snd.op) :
              (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
            x :
          (fun (X : Type u_1) ↦ X) (F.obj (op c.pt))) :
      F.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₂.op) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
        x :
      (fun (X : Type u_1) ↦ X) (F.obj (op Z)))

Tactic:
simp [← comp_apply, ← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} Cᵒᵖ (Type u_1)
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ ∀ (x : F.obj (op X)),
    (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
        p₁ ≫ f = p₂ ≫ f →
          Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₁.op) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
                x :
              (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₂.op) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
                x :
              (fun (X : Type u_1) ↦ X) (F.obj (op Z)))) ↔
      Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.fst.op) :
              (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
            x :
          (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.snd.op) :
              (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
            x :
          (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))

Tactic:
have h (x : F.obj (op X)) : (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
      p₁ ≫ f = p₂ ≫ f → F.map p₁.op x = F.map p₂.op x) ↔ F.map c.fst.op x = F.map c.snd.op x := by
    refine ⟨fun H ↦ H _ _ c.condition, fun H Z p₁ p₂ h ↦ ?_⟩
    rw [← PullbackCone.IsLimit.lift_fst hc _ _ h, op_comp, Functor.map_comp, comp_apply, H]
    simp [← comp_apply, ← Functor.map_comp, ← op_comp]
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X_1 : C
R : Presieve.{v, u} X_1
S : Sieve.{v, u} X_1
inst_1 : R.HasPairwisePullbacks
F : Functor.{v, u_1, u, u_1 + 1} Cᵒᵖ (Type u_1)
X Y : C
f : X ⟶ Y
inst_2 : HasPullback f f
⊢ Eq (α := F.obj (op Y) ⟶ F.obj (op (Limits.pullback f f))) (F.map f.op ≫ F.map (Quiver.Hom.op (pullback.fst f f)))
    (F.map f.op ≫ F.map (Quiver.Hom.op (pullback.snd f f)))

Tactic:
simp [← Functor.map_comp, ← op_comp, pullback.condition]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} Cᵒᵖ (Type u_1)
X Y : C
f : X ⟶ Y
inst_1 : HasPullback f f
⊢ Presieve.IsSheafFor F (Presieve.singleton f) ↔
    Nonempty
      (IsLimit (F :=
        parallelPair (Y := F.obj (op (Limits.pullback f f))) (F.map (Quiver.Hom.op (pullback.fst f f)))
          (F.map (Quiver.Hom.op (pullback.snd f f))))
        (Fork.ofι (F.map f.op) ⋯))

Tactic:
isSheafFor_singleton_iff (pullback.cone f f) (pullback.isLimit f f)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff, CategoryTheory.Limits.pullback.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.pullback.cone
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e_1 : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsEquivalence
U : C
e : Equivalence.{v₁, v₂, u₁, u₂} C D := G.asEquivalence.symm
⊢ ⊤ ∈ (J : (a : C) → Set (Sieve a)) U

Tactic:
J.top_mem U

Premises used: CategoryTheory.GrothendieckTopology.top_mem
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e_1 : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsEquivalence
U : C
e : Equivalence.{v₁, v₂, u₁, u₂} C D := G.asEquivalence.symm
h : Sieve.coverByImage G U = ⊤
⊢ Sieve.coverByImage G U ∈ (J : (a : C) → Set (Sieve a)) U

Tactic:
convert! J.top_mem U

Premises used: CategoryTheory.GrothendieckTopology.top_mem
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e_1 : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsEquivalence
U : C
e : Equivalence.{v₁, v₂, u₁, u₂} C D := G.asEquivalence.symm
h : ∀ ⦃Y : C⦄ (f : Y ⟶ U), (Sieve.coverByImage G U).arrows f ↔ Sieve.arrows ⊤ f
⊢ Sieve.coverByImage G U = ⊤

Tactic:
ext Y f
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e_1 : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsEquivalence
U : C
e : Equivalence.{v₁, v₂, u₁, u₂} C D := G.asEquivalence.symm
Y : C
f : Y ⟶ U
h : (Sieve.coverByImage G U).arrows f
⊢ (Sieve.coverByImage G U).arrows f ↔ Sieve.arrows ⊤ f

Tactic:
simp only [Sieve.top_apply, iff_true]

Premises used: CategoryTheory.Sieve.top_apply, iff_true
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e_1 : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsEquivalence
U : C
e : Equivalence.{v₁, v₂, u₁, u₂} C D := G.asEquivalence.symm
Y : C
f : Y ⟶ U
g : e.inverse.obj (e.functor.obj Y) ⟶ U := e.unitInv.app Y ≫ f
⊢ (Sieve.coverByImage e.inverse U).arrows g

Tactic:
have : (Sieve.coverByImage e.inverse U).arrows g := Presieve.in_coverByImage _ g
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e_1 : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsEquivalence
U : C
e : Equivalence.{v₁, v₂, u₁, u₂} C D := G.asEquivalence.symm
Y : C
f : Y ⟶ U
g : e.inverse.obj (e.functor.obj Y) ⟶ U := e.unitInv.app Y ≫ f
this : (Sieve.coverByImage e.inverse U).arrows g
⊢ (Sieve.coverByImage e.inverse U).arrows (e.unit.app Y ≫ g)

Tactic:
replace := Sieve.downward_closed _ this (e.unit.app Y)
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e_1 : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsEquivalence
U : C
e : Equivalence.{v₁, v₂, u₁, u₂} C D := G.asEquivalence.symm
Y : C
f : Y ⟶ U
g : e.inverse.obj (e.functor.obj Y) ⟶ U := e.unitInv.app Y ≫ f
this : (Sieve.coverByImage e.inverse U).arrows (e.unit.app Y ≫ g)
⊢ (Sieve.coverByImage G U).arrows f

Tactic:
simpa [g] using this
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
h :
  ∀ (X : C) (S : Sieve.{v₁, u₁} X),
    S ∈ (J : (a : C) → Set (Sieve a)) X ↔
      S ∈ (e.functor.inducedTopology (e.inverse.inducedTopology J) : (a : C) → Set (Sieve a)) X
⊢ J = e.functor.inducedTopology (e.inverse.inducedTopology J)

Tactic:
ext X S
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
X : C
S : Sieve.{v₁, u₁} X
h :
  S ∈ (J : (a : C) → Set (Sieve a)) X ↔
    Membership.mem (γ := Set (Sieve.{v₁, u₁} (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X)))
      ((J : (a : C) → Set (Sieve a)) (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X))
      (Sieve.pullback (e.unit.app X) (Sieve.functorPushforward e.inverse (Sieve.functorPushforward e.functor S)))
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X ↔
    S ∈ (e.functor.inducedTopology (e.inverse.inducedTopology J) : (a : C) → Set (Sieve a)) X

Tactic:
rw [show S ∈ (e.functor.inducedTopology (e.inverse.inducedTopology J)) X ↔ _
      from (GrothendieckTopology.pullback_mem_iff_of_isIso (i := e.unit.app X)).symm]

Premises used: CategoryTheory.GrothendieckTopology.pullback_mem_iff_of_isIso, Iff.symm
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
X : C
S : Sieve.{v₁, u₁} X
h :
  Sieve.{v₁, u₁} X = Sieve.{v₁, u₁} (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) →
    S = Sieve.pullback (e.unit.app X) (Sieve.functorPushforward e.inverse (Sieve.functorPushforward e.functor S))
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X ↔
    Membership.mem (γ := Set (Sieve.{v₁, u₁} (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X)))
      ((J : (a : C) → Set (Sieve a)) (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X))
      (Sieve.pullback (e.unit.app X) (Sieve.functorPushforward e.inverse (Sieve.functorPushforward e.functor S)))

Tactic:
congr!
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
X : C
S : Sieve.{v₁, u₁} X
e_1 : Sieve.{v₁, u₁} X = Sieve.{v₁, u₁} (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X)
Y : C
f : Y ⟶ X
⊢ S.arrows f ↔
    (Sieve.pullback (e.unit.app X) (Sieve.functorPushforward e.inverse (Sieve.functorPushforward e.functor S))).arrows f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
⊢ J = e.functor.inducedTopology (e.inverse.inducedTopology J)

Tactic:
have : J = e.functor.inducedTopology (e.inverse.inducedTopology J) := by
    ext X S
    rw [show S ∈ (e.functor.inducedTopology (e.inverse.inducedTopology J)) X ↔ _
      from (GrothendieckTopology.pullback_mem_iff_of_isIso (i := e.unit.app X)).symm]
    congr!; ext Y f; simp
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
this : J = e.functor.inducedTopology (e.inverse.inducedTopology J)
nth_rw :
  IsDenseSubsite (e.functor.inducedTopology (e.inverse.inducedTopology J)) (e.inverse.inducedTopology J) e.functor
⊢ IsDenseSubsite J (e.inverse.inducedTopology J) e.functor

Tactic:
nth_rw 1 [this]
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
this : J = e.functor.inducedTopology (e.inverse.inducedTopology J)
⊢ IsDenseSubsite (e.functor.inducedTopology (e.inverse.inducedTopology J)) (e.inverse.inducedTopology J) e.functor

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : IsDenseSubsite K J e.inverse
h :
  ∀ (x : D) (x_1 : Sieve.{v₂, u₂} x),
    x_1 ∈ (K : (a : D) → Set (Sieve a)) x ↔ x_1 ∈ (e.inverse.inducedTopology J : (a : D) → Set (Sieve a)) x
⊢ K = e.inverse.inducedTopology J

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : IsDenseSubsite K J e.inverse
x : D
x_1 : Sieve.{v₂, u₂} x
⊢ x_1 ∈ (K : (a : D) → Set (Sieve a)) x ↔ x_1 ∈ (e.inverse.inducedTopology J : (a : D) → Set (Sieve a)) x

Tactic:
(e.inverse.functorPushforward_mem_iff K J).symm

Premises used: CategoryTheory.Functor.functorPushforward_mem_iff, Set.Mem, setOf, Iff.symm, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : IsDenseSubsite K J e.inverse
x : D
x_1 : Sieve.{v₂, u₂} x
⊢ x_1 ∈ (K : (a : D) → Set (Sieve a)) x ↔ x_1 ∈ (e.inverse.inducedTopology J : (a : D) → Set (Sieve a)) x

Tactic:
exact (e.inverse.functorPushforward_mem_iff K J).symm

Premises used: CategoryTheory.Functor.functorPushforward_mem_iff, Iff.symm, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : e.functor.IsCocontinuous J K
inst_3 : e.inverse.IsCocontinuous K J
X : C
S : Sieve.{v₁, u₁} X
mp :
  Membership.mem (γ := Set (Sieve.{v₂, u₂} (e.functor.obj X))) ((K : (a : D) → Set (Sieve a)) (e.functor.obj X))
      (Sieve.functorPushforward e.functor S) →
    S ∈ (J : (a : C) → Set (Sieve a)) X
mpr :
  S ∈ (J : (a : C) → Set (Sieve a)) X →
    Membership.mem (γ := Set (Sieve.{v₂, u₂} (e.functor.obj X))) ((K : (a : D) → Set (Sieve a)) (e.functor.obj X))
      (Sieve.functorPushforward e.functor S)
⊢ Membership.mem (γ := Set (Sieve.{v₂, u₂} (e.functor.obj X))) ((K : (a : D) → Set (Sieve a)) (e.functor.obj X))
      (Sieve.functorPushforward e.functor S) ↔
    S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : e.functor.IsCocontinuous J K
inst_3 : e.inverse.IsCocontinuous K J
X : C
S : Sieve.{v₁, u₁} X
H :
  Membership.mem (γ := Set (Sieve.{v₂, u₂} (e.functor.obj X))) ((K : (a : D) → Set (Sieve a)) (e.functor.obj X))
    (Sieve.functorPushforward e.functor S)
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
J.superset_covering ?_ (e.functor.cover_lift J K H)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.cover_lift
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : e.functor.IsCocontinuous J K
inst_3 : e.inverse.IsCocontinuous K J
X : C
S : Sieve.{v₁, u₁} X
H :
  Membership.mem (γ := Set (Sieve.{v₂, u₂} (e.functor.obj X))) ((K : (a : D) → Set (Sieve a)) (e.functor.obj X))
    (Sieve.functorPushforward e.functor S)
mp : Sieve.functorPullback e.functor (Sieve.functorPushforward e.functor S) ≤ S
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
refine J.superset_covering ?_ (e.functor.cover_lift J K H)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.cover_lift
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : e.functor.IsCocontinuous J K
inst_3 : e.inverse.IsCocontinuous K J
X : C
S : Sieve.{v₁, u₁} X
H :
  Membership.mem (γ := Set (Sieve.{v₂, u₂} (e.functor.obj X))) ((K : (a : D) → Set (Sieve a)) (e.functor.obj X))
    (Sieve.functorPushforward e.functor S)
mp mp₁ : S ≤ S
⊢ Sieve.functorPullback e.functor (Sieve.functorPushforward e.functor S) ≤ S

Tactic:
rw [(Sieve.fullyFaithfulFunctorGaloisCoinsertion e.functor X).u_l_eq S]

Premises used: CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion, CategoryTheory.Equivalence.functor, GaloisCoinsertion.u_l_eq
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : e.functor.IsCocontinuous J K
inst_3 : e.inverse.IsCocontinuous K J
X : C
S : Sieve.{v₁, u₁} X
H : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Membership.mem (γ := Set (Sieve.{v₂, u₂} (e.functor.obj X))) ((K : (a : D) → Set (Sieve a)) (e.functor.obj X))
    (Sieve.functorPushforward e.functor S)

Tactic:
K.superset_covering ?_
        (e.inverse.cover_lift K J (J.pullback_stable (e.unitInv.app X) H))

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Equivalence.unitInv, CategoryTheory.Functor.cover_lift, CategoryTheory.NatTrans.app, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : e.functor.IsCocontinuous J K
inst_3 : e.inverse.IsCocontinuous K J
X : C
S : Sieve.{v₁, u₁} X
H : S ∈ (J : (a : C) → Set (Sieve a)) X
mpr : Sieve.functorPullback e.inverse (Sieve.pullback (e.unitInv.app X) S) ≤ Sieve.functorPushforward e.functor S
⊢ Membership.mem (γ := Set (Sieve.{v₂, u₂} (e.functor.obj X))) ((K : (a : D) → Set (Sieve a)) (e.functor.obj X))
    (Sieve.functorPushforward e.functor S)

Tactic:
refine K.superset_covering ?_
        (e.inverse.cover_lift K J (J.pullback_stable (e.unitInv.app X) H))

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Equivalence.unitInv, CategoryTheory.Functor.cover_lift, CategoryTheory.NatTrans.app, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : e.functor.IsCocontinuous J K
inst_3 : e.inverse.IsCocontinuous K J
X : C
S : Sieve.{v₁, u₁} X
H_1 : S ∈ (J : (a : C) → Set (Sieve a)) X
Y : D
f : Y ⟶ e.functor.obj X
H : S.arrows (e.inverse.map f ≫ e.unitInv.app X)
⊢ f = e.counitInv.app Y ≫ e.functor.map (e.inverse.map f ≫ e.unitInv.app X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : e.functor.IsCocontinuous J K
inst_3 : e.inverse.IsCocontinuous K J
X : C
S : Sieve.{v₁, u₁} X
H : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Sieve.functorPullback e.inverse (Sieve.pullback (e.unitInv.app X) S) ≤ Sieve.functorPushforward e.functor S

Tactic:
exact fun Y f (H : S _) ↦ ⟨_, _, e.counitInv.app Y, H, by simp⟩