awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
B : C
I : Type t
inst_1 : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst_2 : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b : Arrows.Compatible P π x
t : P.obj (op B)
⊢ (∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t = x i) ↔
    (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
          (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
        (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
                (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
              (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                  (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                t :
              ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
          Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) =
      x
have h : (∀ (i : I),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t = x i) →
  (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
        (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
      (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
              (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
            (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              t :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
        Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) =
    x
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
B : C
I : Type t
inst_1 : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst_2 : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b : Arrows.Compatible P π x
t : P.obj (op B)
h :
  (∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t = x i) →
    (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
          (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
        (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
                (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
              (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                  (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                t :
              ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
          Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) =
      x
⊢ (∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t = x i) ↔
    (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
          (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
        (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
                (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
              (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                  (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                t :
              ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
          Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) =
      x
have h₁ : (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
        (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
      (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
              (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
            (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              t :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
        Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) =
    x →
  ∀ (i : I), (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t = x i
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
B : C
I : Type t
inst_1 : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst_2 : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b : Arrows.Compatible P π x
t : P.obj (op B)
q :
  ∀ (i : I), (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t = x i
⊢ (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
        (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
      (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
              (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
            (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              t :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
        Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) =
    x
have h : ∀ (i : I),
  (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
        (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
      (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
              (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
            (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              t :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
        Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
      i =
    x i
Tactic: funext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
B : C
I : Type t
inst_1 : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst_2 : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b : Arrows.Compatible P π x
t : P.obj (op B)
q :
  (Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
        (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
      (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
              (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
            (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              t :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
        Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) =
    x
i : I
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t = x i
have h : Eq (α := P.obj (op (X i)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t :
    P.obj (op (X i)))
  ((Equiv.symm (equivShrink ((j : I) → P.obj (op (X j)))) :
        (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → (j : I) → P.obj (op (X j)))
      (((Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i))) :
              (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
            (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              t :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
        Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
      i :
    P.obj (op (X i)))
Tactic: rw [← q]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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)))
have refine : ∀
  (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 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: refine ⟨fun H ↦ H _ _ c.condition, fun H Z p₁ p₂ h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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 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)))
have 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)))
Tactic: rw [← PullbackCone.IsLimit.lift_fst hc _ _ h, op_comp, Functor.map_comp, comp_apply, H]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (hypothesis)
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
⊢ Presieve.IsSheafFor F (Presieve.singleton f) ↔ Nonempty (IsLimit (Fork.ofι (F.map f.op) ⋯))
have h : ∀ (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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
⊢ Sieve.coverByImage G U ∈ (J : (a : C) → Set (Sieve a)) U
have h : Sieve.coverByImage G U = ⊤
Tactic: convert! J.top_mem U
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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
⊢ Sieve.coverByImage G U = ⊤
have h : ∀ ⦃Y : C⦄ (f : Y ⟶ U), (Sieve.coverByImage G U).arrows f ↔ Sieve.arrows ⊤ f
Tactic: ext Y f
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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
⊢ (Sieve.coverByImage G U).arrows f ↔ Sieve.arrows ⊤ f
have h : (Sieve.coverByImage G U).arrows f
Tactic: simp only [Sieve.top_apply, iff_true]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (hypothesis)
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 G U).arrows f
have this : (Sieve.coverByImage e.inverse U).arrows g
Tactic: have : (Sieve.coverByImage e.inverse U).arrows g := Presieve.in_coverByImage _ g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (hypothesis)
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 G U).arrows f
have this₁ : (Sieve.coverByImage e.inverse U).arrows (e.unit.app Y ≫ g)
Tactic: replace := Sieve.downward_closed _ this (e.unit.app Y)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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)
have 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
Tactic: ext X S
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X ↔
    S ∈ (e.functor.inducedTopology (e.inverse.inducedTopology J) : (a : C) → Set (Sieve a)) X
have 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)))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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
⊢ 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)))
have 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))
Tactic: congr!
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (hypothesis)
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
⊢ IsDenseSubsite J (e.inverse.inducedTopology J) e.functor
have this : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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 J (e.inverse.inducedTopology J) e.functor
have nth_rw : IsDenseSubsite (e.functor.inducedTopology (e.inverse.inducedTopology J)) (e.inverse.inducedTopology J) e.functor
Tactic: nth_rw 1 [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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
⊢ K = e.inverse.inducedTopology J
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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
⊢ 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
have 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
Tactic: constructor