awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s_1 :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (x : ULift.{w, 0} WalkingPair) ↦
    match (motive := ULift.{w, 0} WalkingPair → Opens (↑X : Type w)) x with
    | { down := j } => WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j U V
hι : U ⊔ V = iSup ι
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a : ULift.{w, 0} WalkingPair
⊢ F.interUnionPullbackConeLift U V s ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (eqToHom ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)) =
    s.fst

Tactic:
apply interUnionPullbackConeLift_left

Premises used: TopCat.Sheaf.interUnionPullbackConeLift_left
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s_1 :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (x : ULift.{w, 0} WalkingPair) ↦
    match (motive := ULift.{w, 0} WalkingPair → Opens (↑X : Type w)) x with
    | { down := j } => WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j U V
hι : U ⊔ V = iSup ι
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a : ULift.{w, 0} WalkingPair
⊢ m ≫ (F.interUnionPullbackCone U V).snd = s.snd

Tactic:
h₂
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s_1 :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (x : ULift.{w, 0} WalkingPair) ↦
    match (motive := ULift.{w, 0} WalkingPair → Opens (↑X : Type w)) x with
    | { down := j } => WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j U V
hι : U ⊔ V = iSup ι
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a : ULift.{w, 0} WalkingPair
h :
  F.interUnionPullbackConeLift U V s ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (eqToHom ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)) =
    s.snd
⊢ Eq (α :=
    s.pt ⟶
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj
        (op (ι { down := WalkingPair.right })))
    (m ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (eqToHom ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)) :
      s.pt ⟶
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj
          (op (ι { down := WalkingPair.right })))
    (F.interUnionPullbackConeLift U V s ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (eqToHom ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)) :
      s.pt ⟶
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj
          (op (ι { down := WalkingPair.right })))

Tactic:
convert! h₂
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s_1 :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (x : ULift.{w, 0} WalkingPair) ↦
    match (motive := ULift.{w, 0} WalkingPair → Opens (↑X : Type w)) x with
    | { down := j } => WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j U V
hι : U ⊔ V = iSup ι
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a : ULift.{w, 0} WalkingPair
⊢ F.interUnionPullbackConeLift U V s ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (eqToHom ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)) =
    s.snd

Tactic:
apply interUnionPullbackConeLift_right

Premises used: TopCat.Sheaf.interUnionPullbackConeLift_right
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
U : Opens (↑X : Type w)
R : Presieve U
f : (V : Opens (↑X : Type w)) × { f : V ⟶ U // R f }
⊢ coveringOfPresieve U R f = f.fst (β := fun (V : Opens (↑X : Type w)) ↦ { f : V ⟶ U // R f })

Tactic:
rfl

Premises used: TopCat.Presheaf.coveringOfPresieve, rfl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
U : Opens (↑X : Type w)
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U
a : iSup (coveringOfPresieve U R) ≤ U
a₁ : U ≤ iSup (coveringOfPresieve U R)
⊢ iSup (coveringOfPresieve U R) = U

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
U : Opens (↑X : Type w)
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U
⊢ iSup (coveringOfPresieve U R) ≤ U

Tactic:
iSup_le ?_

Premises used: Set.Mem, iSup_le
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
U : Opens (↑X : Type w)
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U
a : ∀ (i : (V : Opens (↑X : Type w)) × { f : V ⟶ U // R f }), coveringOfPresieve U R i ≤ U
⊢ iSup (coveringOfPresieve U R) ≤ U

Tactic:
refine iSup_le ?_

Premises used: iSup_le
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
U : Opens (↑X : Type w)
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U
f : (V : Opens (↑X : Type w)) × { f : V ⟶ U // R f }
⊢ coveringOfPresieve U R f ≤ U

Tactic:
f.2.1.le

Premises used: Set.Mem, Quiver.Hom.le, Sigma.snd, Subtype.val
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
U : Opens (↑X : Type w)
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U
f : (V : Opens (↑X : Type w)) × { f : V ⟶ U // R f }
⊢ coveringOfPresieve U R f ≤ U

Tactic:
exact f.2.1.le

Premises used: Quiver.Hom.le, Sigma.snd, Subtype.val
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
U : Opens (↑X : Type w)
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U
x : (↑X : Type w)
hxU : x ∈ U
a : ∃ (i : (V : Opens (↑X : Type w)) × { f : V ⟶ U // R f }), x ∈ coveringOfPresieve U R i
⊢ x ∈ iSup (coveringOfPresieve U R)

Tactic:
rw [Opens.mem_iSup]

Premises used: TopologicalSpace.Opens.mem_iSup
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
U : Opens (↑X : Type w)
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U
x : (↑X : Type w)
hxU : x ∈ U
a :
  ∀ (V : Opens (↑X : Type w)) (iVU : V ⟶ U) (hxV : x ∈ V) (W : Opens (↑X : Type w)) (iVW : V ⟶ W) (iWU : W ⟶ U)
    (hiWU : R iWU), ∃ (i : (V : Opens (↑X : Type w)) × { f : V ⟶ U // R f }), x ∈ coveringOfPresieve U R i
⊢ ∃ (i : (V : Opens (↑X : Type w)) × { f : V ⟶ U // R f }), x ∈ coveringOfPresieve U R i

Tactic:
obtain ⟨V, iVU, ⟨W, iVW, iWU, hiWU, -⟩, hxV⟩ := hR x hxU
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
U : Opens (↑X : Type w)
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U
x : (↑X : Type w)
hxU : x ∈ U
V : Opens (↑X : Type w)
iVU : V ⟶ U
hxV : x ∈ V
W : Opens (↑X : Type w)
iVW : V ⟶ W
iWU : W ⟶ U
hiWU : R iWU
⊢ ∃ (i : (V : Opens (↑X : Type w)) × { f : V ⟶ U // R f }), x ∈ coveringOfPresieve U R i

Tactic:
⟨⟨W, ⟨iWU, hiWU⟩⟩, iVW.le hxV⟩

Premises used: Quiver.Hom.le, Subtype.mk, Exists.intro, Sigma.mk
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
U : Opens (↑X : Type w)
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U
x : (↑X : Type w)
hxU : x ∈ U
V : Opens (↑X : Type w)
iVU : V ⟶ U
hxV : x ∈ V
W : Opens (↑X : Type w)
iVW : V ⟶ W
iWU : W ⟶ U
hiWU : R iWU
⊢ ∃ (i : (V : Opens (↑X : Type w)) × { f : V ⟶ U // R f }), x ∈ coveringOfPresieve U R i

Tactic:
exact ⟨⟨W, ⟨iWU, hiWU⟩⟩, iVW.le hxV⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
Y : Opens (↑X : Type w)
R : Presieve Y
h : ∀ (Z : Opens (↑X : Type w)), Eq (α := (Z ⟶ Y) → Prop) (presieveOfCoveringAux (coveringOfPresieve Y R) Y) R
⊢ presieveOfCoveringAux (coveringOfPresieve Y R) Y = R

Tactic:
funext Z
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
Y : Opens (↑X : Type w)
R : Presieve Y
Z : Opens (↑X : Type w)
h : ∀ (f : Z ⟶ Y), presieveOfCoveringAux (coveringOfPresieve Y R) Y f ↔ R f
⊢ Eq (α := (Z ⟶ Y) → Prop) (presieveOfCoveringAux (coveringOfPresieve Y R) Y) R

Tactic:
ext f
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
Y : Opens (↑X : Type w)
R : Presieve Y
Z : Opens (↑X : Type w)
f : Z ⟶ Y
h_1 : presieveOfCoveringAux (coveringOfPresieve Y R) Y f
f' : Z ⟶ Y
h rwa rwa₁ rwa₂ rwa₃ : R f'
⊢ R f

Tactic:
rwa [Subsingleton.elim f f']

Premises used: Subsingleton.elim
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
Y : Opens (↑X : Type w)
R : Presieve Y
Z : Opens (↑X : Type w)
f : Z ⟶ Y
⊢ presieveOfCoveringAux (coveringOfPresieve Y R) Y f ↔ R f

Tactic:
exact ⟨fun ⟨⟨_, f', h⟩, rfl⟩ => by rwa [Subsingleton.elim f f'], fun h => ⟨⟨Z, f, h⟩, rfl⟩⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
ι : Type v
U : ι → Opens (↑X : Type w)
x : (↑X : Type w)
hx : x ∈ iSup U
obtain :
  ∀ (i : ι) (hxi : x ∈ U i),
    ∃ (U_1 : Opens (↑X : Type w)) (f : U_1 ⟶ iSup U), (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1
⊢ ∃ (U_1 : Opens (↑X : Type w)) (f : U_1 ⟶ iSup U), (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1

Tactic:
obtain ⟨i, hxi⟩ := Opens.mem_iSup.mp hx

Premises used: TopologicalSpace.Opens.mem_iSup, Iff.mp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
ι : Type v
U : ι → Opens (↑X : Type w)
x : (↑X : Type w)
hx : x ∈ iSup U
i : ι
hxi : x ∈ U i
⊢ ∃ (U_1 : Opens (↑X : Type w)) (f : U_1 ⟶ iSup U), (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1

Tactic:
⟨U i, Opens.leSupr U i, ⟨U i, 𝟙 _, Opens.leSupr U i, ⟨i, rfl⟩, Category.id_comp _⟩, hxi⟩

Premises used: CategoryTheory.CategoryStruct.id, TopologicalSpace.Opens.leSupr, And.intro, Exists.intro, rfl, CategoryTheory.Category.id_comp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
ι : Type v
U : ι → Opens (↑X : Type w)
x : (↑X : Type w)
hx : x ∈ iSup U
i : ι
hxi : x ∈ U i
⊢ ∃ (U_1 : Opens (↑X : Type w)) (f : U_1 ⟶ iSup U), (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1

Tactic:
exact ⟨U i, Opens.leSupr U i, ⟨U i, 𝟙 _, Opens.leSupr U i, ⟨i, rfl⟩, Category.id_comp _⟩, hxi⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
ι : Type v
U : ι → Opens (↑X : Type w)
f : (V : Opens (↑X : Type w)) × { f : V ⟶ iSup U // presieveOfCovering U f }
⊢ f.fst (β := fun (V : Opens (↑X : Type w)) ↦ { f : V ⟶ iSup U // presieveOfCovering U f }) = U (indexOfHom U f)

Tactic:
f.2.2.choose_spec

Premises used: Exists.choose_spec, TopCat.Presheaf.presieveOfCovering.indexOfHom, Sigma.snd, Subtype.property
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
ι : Type u_1
inst : Category.{v_1, u_1} ι
B : CategoryTheory.Functor.{v_1, w, u_1, w} ι (Opens (↑X : Type w))
rw :
  B.IsCoverDense (Opens.grothendieckTopology (↑X : Type w)) ↔
    ∀ {U : Opens (↑X : Type w)} {x : (↑X : Type w)}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
⊢ B.IsCoverDense (Opens.grothendieckTopology (↑X : Type w)) ↔ Opens.IsBasis (Set.range B.obj)

Tactic:
rw [Opens.isBasis_iff_nbhd]

Premises used: TopologicalSpace.Opens.isBasis_iff_nbhd
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
ι : Type u_1
inst : Category.{v_1, u_1} ι
B : CategoryTheory.Functor.{v_1, w, u_1, w} ι (Opens (↑X : Type w))
mp :
  B.IsCoverDense (Opens.grothendieckTopology (↑X : Type w)) →
    ∀ {U : Opens (↑X : Type w)} {x : (↑X : Type w)}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
mpr :
  (∀ {U : Opens (↑X : Type w)} {x : (↑X : Type w)}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U) →
    B.IsCoverDense (Opens.grothendieckTopology (↑X : Type w))
⊢ B.IsCoverDense (Opens.grothendieckTopology (↑X : Type w)) ↔
    ∀ {U : Opens (↑X : Type w)} {x : (↑X : Type w)}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U

Tactic:
constructor
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
ι : Type u_1
inst : Category.{v_1, u_1} ι
B : CategoryTheory.Functor.{v_1, w, u_1, w} ι (Opens (↑X : Type w))
hd : B.IsCoverDense (Opens.grothendieckTopology (↑X : Type w))
U : Opens (↑X : Type w)
x : (↑X : Type w)
hx : x ∈ U
mp :
  ∀ (V : Opens (↑X : Type w)) (f : V ⟶ U) (hV : x ∈ V) (i : ι) (f₁ : V ⟶ B.obj i) (f₂ : B.obj i ⟶ U),
    f₁ ≫ f₂ = f → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
⊢ ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U

Tactic:
rcases hd.1 U x hx with ⟨V, f, ⟨i, f₁, f₂, _⟩, hV⟩

Premises used: CategoryTheory.Functor.IsCoverDense.is_cover
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
ι : Type u_1
inst : Category.{v_1, u_1} ι
B : CategoryTheory.Functor.{v_1, w, u_1, w} ι (Opens (↑X : Type w))
hd : B.IsCoverDense (Opens.grothendieckTopology (↑X : Type w))
U : Opens (↑X : Type w)
x : (↑X : Type w)
hx : x ∈ U
V : Opens (↑X : Type w)
f : V ⟶ U
hV : x ∈ V
i : ι
f₁ : V ⟶ B.obj i
f₂ : B.obj i ⟶ U
fac : f₁ ≫ f₂ = f
⊢ ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U

Tactic:
⟨B.obj i, ⟨i, rfl⟩, f₁.le hV, f₂.le⟩

Premises used: Quiver.Hom.le, And.intro, Exists.intro, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
ι : Type u_1
inst : Category.{v_1, u_1} ι
B : CategoryTheory.Functor.{v_1, w, u_1, w} ι (Opens (↑X : Type w))
hd : B.IsCoverDense (Opens.grothendieckTopology (↑X : Type w))
U : Opens (↑X : Type w)
x : (↑X : Type w)
hx : x ∈ U
V : Opens (↑X : Type w)
f : V ⟶ U
hV : x ∈ V
i : ι
f₁ : V ⟶ B.obj i
f₂ : B.obj i ⟶ U
fac : f₁ ≫ f₂ = f
⊢ ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U

Tactic:
exact ⟨B.obj i, ⟨i, rfl⟩, f₁.le hV, f₂.le⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
ι : Type u_1
inst : Category.{v_1, u_1} ι
B : CategoryTheory.Functor.{v_1, w, u_1, w} ι (Opens (↑X : Type w))
hb : ∀ {U : Opens (↑X : Type w)} {x : (↑X : Type w)}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
mpr :
  ∀ (U : Opens (↑X : Type w)),
    Sieve.coverByImage B U ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U
⊢ B.IsCoverDense (Opens.grothendieckTopology (↑X : Type w))

Tactic:
constructor
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
ι : Type u_1
inst : Category.{v_1, u_1} ι
B : CategoryTheory.Functor.{v_1, w, u_1, w} ι (Opens (↑X : Type w))
hb : ∀ {U : Opens (↑X : Type w)} {x : (↑X : Type w)}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
U : Opens (↑X : Type w)
x : (↑X : Type w)
hx : x ∈ U
mpr :
  ∀ (i : ι) (hx : x ∈ B.obj i) (hi : B.obj i ≤ U),
    ∃ (U_1 : Opens (↑X : Type w)) (f : U_1 ⟶ U), (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1
⊢ ∃ (U_1 : Opens (↑X : Type w)) (f : U_1 ⟶ U), (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1

Tactic:
rcases hb hx with ⟨_, ⟨i, rfl⟩, hx, hi⟩

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
ι : Type u_1
inst : Category.{v_1, u_1} ι
B : CategoryTheory.Functor.{v_1, w, u_1, w} ι (Opens (↑X : Type w))
hb : ∀ {U : Opens (↑X : Type w)} {x : (↑X : Type w)}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
U : Opens (↑X : Type w)
x : (↑X : Type w)
hx_1 : x ∈ U
i : ι
hx : x ∈ B.obj i
hi : B.obj i ≤ U
⊢ ∃ (U_1 : Opens (↑X : Type w)) (f : U_1 ⟶ U), (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1

Tactic:
⟨B.obj i, ⟨⟨hi⟩⟩, ⟨⟨i, 𝟙 _, ⟨⟨hi⟩⟩, rfl⟩⟩, hx⟩

Premises used: CategoryTheory.CategoryStruct.id, Nonempty.intro, PLift.up, And.intro, Exists.intro, CategoryTheory.Presieve.CoverByImageStructure.mk, ULift.up, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
ι : Type u_1
inst : Category.{v_1, u_1} ι
B : CategoryTheory.Functor.{v_1, w, u_1, w} ι (Opens (↑X : Type w))
hb : ∀ {U : Opens (↑X : Type w)} {x : (↑X : Type w)}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
U : Opens (↑X : Type w)
x : (↑X : Type w)
hx_1 : x ∈ U
i : ι
hx : x ∈ B.obj i
hi : B.obj i ≤ U
⊢ ∃ (U_1 : Opens (↑X : Type w)) (f : U_1 ⟶ U), (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1

Tactic:
exact ⟨B.obj i, ⟨⟨hi⟩⟩, ⟨⟨i, 𝟙 _, ⟨⟨hi⟩⟩, rfl⟩⟩, hx⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X : TopCat
ι : Type u_1
B : ι → Opens (↑X : Type w)
h : Opens.IsBasis (Set.range B)
⊢ Functor.IsCoverDense (inducedFunctor B) (Opens.grothendieckTopology (↑X : Type w))

Tactic:
(coverDense_iff_isBasis _).2 h

Premises used: Iff.mpr, TopCat.Opens.coverDense_iff_isBasis
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
⊢ Mono f

Tactic:
haveI : Mono f := (TopCat.mono_iff_injective f).mpr hf.injective
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
this : Mono f
hF :
  {c : Opens (↑X : Type w)} →
    {d : Opens (↑Y : Type w)} → (d ⟶ hf.functor.obj c) → (c' : Opens (↑X : Type w)) × (hf.functor.obj c' ≅ d)
⊢ CompatiblePreserving (Opens.grothendieckTopology (↑Y : Type w)) hf.functor

Tactic:
apply compatiblePreservingOfDownwardsClosed

Premises used: CategoryTheory.compatiblePreservingOfDownwardsClosed
-- Module: Mathlib.Topology.Sheaves.SheafCondition.Sites
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
this : Mono f
U : Opens (↑X : Type w)
V : Opens (↑Y : Type w)
i : V ⟶ hf.functor.obj U
hF :
  ∀ (x : (↑Y : Type w)) (h : Membership.mem (γ := Set (↑Y : Type w)) V.1 x),
    Membership.mem (γ := Set (↑Y : Type w))
      (Set.range (ι := (↑X : Type w))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
              f) :
          (a : (↑X : Type w)) → (↑Y : Type w)))
      x
⊢ (c' : Opens (↑X : Type w)) × (hf.functor.obj c' ≅ V)

Tactic:
refine ⟨(Opens.map f).obj V, eqToIso <| Opens.ext <| Set.image_preimage_eq_of_subset fun x h ↦ ?_⟩