awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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
⊢ Eq (α :=
    s.pt ⟶ (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := WalkingPair.right })))
    (m ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (eqToHom ⋯) ≫
          NatTrans.app (Cone.π (Cocone.op (Pairwise.cocone ι))) (op (Pairwise.single { down := WalkingPair.right }))))
    (F.interUnionPullbackConeLift U V s ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (eqToHom ⋯) ≫
          NatTrans.app (Cone.π (Cocone.op (Pairwise.cocone ι))) (op (Pairwise.single { down := WalkingPair.right }))))
have h : (s.pt ⟶
      (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj
        (op (Pairwise.single { down := WalkingPair.right : ULift.{w, 0} WalkingPair }))) =
    (s.pt ⟶ F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V)) →
  F.interUnionPullbackConeLift U V s ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (eqToHom sorry) ≫
          NatTrans.app (Cone.π (Cocone.op (Pairwise.cocone ι))) (op (Pairwise.single { down := WalkingPair.right }))) =
    s.snd
Tactic: convert! h₂
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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
⊢ Eq (α :=
    s.pt ⟶
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj
        (op (ι { down := WalkingPair.left })))
    (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.left })))
    (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.left })))
have h : F.interUnionPullbackConeLift U V s ≫
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (eqToHom sorry) ≫ Quiver.Hom.op (homOfLE sorry)) =
  s.fst
Tactic: convert! h₁
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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
⊢ 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 })))
have h : F.interUnionPullbackConeLift U V s ≫
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (eqToHom sorry) ≫ Quiver.Hom.op (homOfLE sorry)) =
  s.snd
Tactic: convert! h₂
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
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
have a : iSup (coveringOfPresieve U R) ≤ U
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
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
⊢ iSup (coveringOfPresieve U R) = U
have a₁ : U ≤ iSup (coveringOfPresieve U R)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
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
have a : ∀ (i : (V : Opens (↑X : Type w)) × { f : V ⟶ U // R f }), coveringOfPresieve U R i ≤ U
Tactic: refine iSup_le ?_
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
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
⊢ x ∈ iSup (coveringOfPresieve U R)
have a : ∃ (i : (V : Opens (↑X : Type w)) × { f : V ⟶ U // R f }), x ∈ coveringOfPresieve U R i
Tactic: rw [Opens.mem_iSup]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
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
⊢ ∃ (i : (V : Opens (↑X : Type w)) × { f : V ⟶ U // R f }), x ∈ coveringOfPresieve U R i
have 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
Tactic: obtain ⟨V, iVU, ⟨W, iVW, iWU, hiWU, -⟩, hxV⟩ := hR x hxU
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
X : TopCat
Y : Opens (↑X : Type w)
R : Presieve Y
⊢ presieveOfCoveringAux (coveringOfPresieve Y R) Y = R
have h : ∀ (Z : Opens (↑X : Type w)), Eq (α := (Z ⟶ Y) → Prop) (presieveOfCoveringAux (coveringOfPresieve Y R) Y) R
Tactic: funext Z
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
X : TopCat
Y : Opens (↑X : Type w)
R : Presieve Y
Z : Opens (↑X : Type w)
⊢ Eq (α := (Z ⟶ Y) → Prop) (presieveOfCoveringAux (coveringOfPresieve Y R) Y) R
have h : ∀ (f : Z ⟶ Y), presieveOfCoveringAux (coveringOfPresieve Y R) Y f ↔ R f
Tactic: ext f
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
X : TopCat
ι : Type v
U : ι → Opens (↑X : Type w)
x : (↑X : Type w)
hx : x ∈ iSup U
⊢ ∃ (U_1 : Opens (↑X : Type w)) (f : U_1 ⟶ iSup U), (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1
have 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
Tactic: obtain ⟨i, hxi⟩ := Opens.mem_iSup.mp hx
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
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))
⊢ B.IsCoverDense (Opens.grothendieckTopology (↑X : Type w)) ↔ Opens.IsBasis (Set.range B.obj)
have 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
Tactic: rw [Opens.isBasis_iff_nbhd]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
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))
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
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
⊢ 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
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
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
⊢ ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
have 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
Tactic: rcases hd.1 U x hx with ⟨V, f, ⟨i, f₁, f₂, _⟩, hV⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
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
⊢ B.IsCoverDense (Opens.grothendieckTopology (↑X : Type w))
have mpr : ∀ (U : Opens (↑X : Type w)),
  Sieve.coverByImage B U ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
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
⊢ ∃ (U_1 : Opens (↑X : Type w)) (f : U_1 ⟶ U), (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1
have 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
Tactic: rcases hb hx with ⟨_, ⟨i, rfl⟩, hx, hi⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (hypothesis)
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))
⊢ CompatiblePreserving (Opens.grothendieckTopology (↑Y : Type w)) hf.functor
have this : Mono f
Tactic: haveI : Mono f := (TopCat.mono_iff_injective f).mpr hf.injective
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
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
⊢ CompatiblePreserving (Opens.grothendieckTopology (↑Y : Type w)) hf.functor
have 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)
Tactic: apply compatiblePreservingOfDownwardsClosed
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
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
⊢ (c' : Opens (↑X : Type w)) × (hf.functor.obj c' ≅ V)
have 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
Tactic: refine ⟨(Opens.map f).obj V, eqToIso <| Opens.ext <| Set.image_preimage_eq_of_subset fun x h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
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
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
have hF : ∀ w ∈ (↑U : Set (↑X : Type w)),
  ∀
    (h :
      Membership.mem (α := (↑Y : Type w)) (γ := Set (↑Y : Type w)) V.1
        ((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))
            w :
          (↑Y : Type w))),
    Membership.mem (α := (↑Y : Type w)) (γ := 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)))
      ((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))
          w :
        (↑Y : Type w))
Tactic: obtain ⟨_, _, rfl⟩ := i.le h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (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))
⊢ CoverPreserving (Opens.grothendieckTopology (↑X : Type w)) (Opens.grothendieckTopology (↑Y : Type w)) hf.functor
have cover_preserve : ∀ {U : Opens (↑X : Type w)} {S : Sieve U},
  S ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U →
    Membership.mem (γ := Set (Sieve (hf.functor.obj U)))
      ((Opens.grothendieckTopology (↑Y : Type w) : (a : Opens (↑Y : Type w)) → Set (Sieve a)) (hf.functor.obj U))
      (Sieve.functorPushforward hf.functor S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (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))
U : Opens (↑X : Type w)
S : Sieve U
hU : S ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U
x : (↑X : Type w)
hx : x ∈ (↑U : Set (↑X : Type w))
⊢ ∃ (U_1 : Opens (↑Y : Type w)) (f_1 : U_1 ⟶ hf.functor.obj U),
    (Sieve.functorPushforward hf.functor S).arrows f_1 ∧
      Membership.mem (α := (↑Y : Type w)) U_1
        ((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 :
          (↑Y : Type w))
have cover_preserve : ∀ (V : Opens (↑X : Type w)) (i : V ⟶ U) (hV : S.arrows i) (hxV : x ∈ V),
  ∃ (U_1 : Opens (↑Y : Type w)) (f_1 : U_1 ⟶ hf.functor.obj U),
    (Sieve.functorPushforward hf.functor S).arrows f_1 ∧
      Membership.mem (α := (↑Y : Type w)) U_1
        ((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 :
          (↑Y : Type w))
Tactic: obtain ⟨V, i, hV, hxV⟩ := hU x hx
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
X Y : TopCat
f : X ⟶ Y
h :
  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))
⊢ h.functor.IsContinuous (Opens.grothendieckTopology (↑X : Type w)) (Opens.grothendieckTopology (↑Y : Type w))
have hF₁ : CompatiblePreserving (Opens.grothendieckTopology (↑Y : Type w)) h.functor
Tactic: apply Functor.isContinuous_of_coverPreserving
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
X Y : TopCat
f : X ⟶ Y
h :
  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))
hF₁ : CompatiblePreserving (Opens.grothendieckTopology (↑Y : Type w)) h.functor
⊢ h.functor.IsContinuous (Opens.grothendieckTopology (↑X : Type w)) (Opens.grothendieckTopology (↑Y : Type w))
have hF₂ : CoverPreserving (Opens.grothendieckTopology (↑X : Type w)) (Opens.grothendieckTopology (↑Y : Type w)) h.functor
Tactic: apply Functor.isContinuous_of_coverPreserving
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : Presheaf.{w, v, u} C Y
h :
  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 := carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
hF : F.IsSheaf
⊢ IsSheaf (h.functor.op ⋙ F)
have this : h.functor.IsContinuous (Opens.grothendieckTopology (↑X : Type w)) (Opens.grothendieckTopology (↑Y : Type w))
Tactic: have := h.functor_isContinuous
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
⊢ RepresentablyFlat (Opens.map f)
have cofiltered : ∀ (X_1 : Opens (↑X : Type w)), IsCofiltered.{w, w} (StructuredArrow X_1 (Opens.map f))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
U : Opens (↑X : Type w)
⊢ IsCofiltered.{w, w} (StructuredArrow U (Opens.map f))
have cofiltered : IsCofilteredOrEmpty.{w, w} (StructuredArrow U (Opens.map f))
Tactic: refine @IsCofiltered.mk _ _ ?_ ?_