awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.MayerVietoris (goal)
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ sq.X₂ ⊔ sq.X₃
inl : ∀ (hx : x ∈ (↑sq.X₂ : Set T)), ∃ (U : Opens T) (f : U ⟶ sq.X₄), (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U
⊢ ∃ (U : Opens T) (f : U ⟶ sq.X₄), (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U
have inr : ∀ (hx : x ∈ (↑sq.X₃ : Set T)), ∃ (U : Opens T) (f : U ⟶ sq.X₄), (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U
Tactic: obtain (hx | hx) := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Over (goal)
Goal:
X : Type u
inst : TopologicalSpace X
U : Opens X
V : Over U
⊢ (Functor.obj (𝟭 (Over U)) V).left =
    Over.left (X := U)
      (Functor.obj
        (Functor.comp (D := Opens ↥U)
          {
            obj := fun (V : Over U) ↦
              { carrier := Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' (↑V.left : Set X), is_open' := ⋯ },
            map := fun {X_1 Y : Over U} (f : X_1 ⟶ Y) ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
          {
            obj := fun (W : Opens ↥U) ↦
              Over.mk (Y := { carrier := Subtype.val (p := fun (x : X) ↦ x ∈ U) '' (↑W : Set ↥U), is_open' := ⋯ })
                (homOfLE ⋯),
            map := fun {X_1 Y : Opens ↥U} (f : X_1 ⟶ Y) ↦ Over.homMk (homOfLE ⋯) ⋯, map_id := ⋯, map_comp := ⋯ })
        V)
have h : ∀ (x : X),
  x ∈ (↑(Functor.obj (𝟭 (Over U)) V).left : Set X) ↔
    x ∈
      (↑(Over.left (X := U)
            (Functor.obj
              (Functor.comp (D := Opens ↥U)
                {
                  obj := fun (V : Over U) ↦
                    { carrier := Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' (↑V.left : Set X), is_open' := sorry :
                      Opens ↥U },
                  map := fun {X_1 Y : Over U} (f : X_1 ⟶ Y) ↦ homOfLE sorry, map_id := sorry, map_comp := sorry :
                  Over U ⥤ Opens ↥U }
                {
                  obj := fun (W : Opens ↥U) ↦
                    Over.mk (Y :=
                      { carrier := Subtype.val (p := fun (x : X) ↦ x ∈ U) '' (↑W : Set ↥U), is_open' := sorry : Opens X })
                      (homOfLE sorry),
                  map := fun {X_1 Y : Opens ↥U} (f : X_1 ⟶ Y) ↦ Over.homMk (homOfLE sorry) sorry, map_id := sorry, map_comp := sorry :
                  Opens ↥U ⥤ Over U })
              V)) :
        Set X)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Over (goal)
Goal:
X : Type u
inst : TopologicalSpace X
U : Opens X
V : Over U
x : X
⊢ x ∈ (↑(Functor.obj (𝟭 (Over U)) V).left : Set X) ↔
    x ∈
      (↑(Over.left (X := U)
            (Functor.obj
              (Functor.comp (D := Opens ↥U)
                {
                  obj := fun (V : Over U) ↦
                    { carrier := Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' (↑V.left : Set X), is_open' := ⋯ :
                      Opens ↥U },
                  map := fun {X_1 Y : Over U} (f : X_1 ⟶ Y) ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ :
                  Over U ⥤ Opens ↥U }
                {
                  obj := fun (W : Opens ↥U) ↦
                    Over.mk (Y :=
                      { carrier := Subtype.val (p := fun (x : X) ↦ x ∈ U) '' (↑W : Set ↥U), is_open' := ⋯ : Opens X })
                      (homOfLE ⋯),
                  map := fun {X_1 Y : Opens ↥U} (f : X_1 ⟶ Y) ↦ Over.homMk (homOfLE ⋯) ⋯, map_id := ⋯, map_comp := ⋯ :
                  Opens ↥U ⥤ Over U })
              V)) :
        Set X)
have h : x ∈ (↑V.left : Set X) ↔
  x ∈
    Set.image (α := ↥U) (Subtype.val (p := fun (x : X) ↦ x ∈ U))
      (Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' (↑V.left : Set X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Over (goal)
Goal:
X : Type u
inst : TopologicalSpace X
U : Opens X
V : Over U
x : X
⊢ x ∈ (↑V.left : Set X) ↔
    x ∈
      Set.image (α := ↥U) (Subtype.val (p := fun (x : X) ↦ x ∈ U))
        (Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' (↑V.left : Set X))
have h : x ∈ V.left → x ∈ U
Tactic: simp only [SetLike.mem_coe, Set.mem_image, Set.mem_preimage,
      Subtype.exists, exists_and_left, exists_prop, exists_eq_right_right, iff_self_and]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.PUnit (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens (↑X : Type w)
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) U
⊢ Presieve.IsSheafFor (F ⋙ Functor.obj coyoneda (op c)) s.arrows
have this : IndiscreteTopology.{w} (↑X : Type w)
Tactic: have : IndiscreteTopology X := ⟨hind⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens (↑X : Type w)
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) U
this : IndiscreteTopology.{w} (↑X : Type w)
⊢ Presieve.IsSheafFor (F ⋙ Functor.obj coyoneda (op c)) s.arrows
have inl : ∀ (s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥)
  (hs :
    Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥))
      ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊥) s),
  Presieve.IsSheafFor (F ⋙ Functor.obj coyoneda (op c)) s.arrows
Tactic: obtain rfl | hne := eq_or_ne U ⊥
Cleared hypotheses: U, s, hs
-- Lean 4 proof step from Mathlib.Topology.Sheaves.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens (↑X : Type w)
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) U
this : IndiscreteTopology.{w} (↑X : Type w)
inl :
  ∀ (s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥)
    (hs :
      Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥))
        ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊥) s),
    Presieve.IsSheafFor (F ⋙ Functor.obj coyoneda (op c)) s.arrows
⊢ Presieve.IsSheafFor (F ⋙ Functor.obj coyoneda (op c)) s.arrows
have inr : ∀ (hne : U ≠ ⊥), Presieve.IsSheafFor (F ⋙ Functor.obj coyoneda (op c)) s.arrows
Tactic: obtain rfl | hne := eq_or_ne U ⊥
-- Lean 4 proof step from Mathlib.Topology.Sheaves.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊥) s
x : Presieve.FamilyOfElements (F ⋙ Functor.obj coyoneda (op c)) s.arrows
h : x.Compatible (R := s.arrows)
⊢ ∃! t : (F ⋙ Functor.obj coyoneda (op c)).obj (op ⊥), x.IsAmalgamation (R := s.arrows) t
have inl : ∃ (x_1 : (F ⋙ Functor.obj coyoneda (op c)).obj (op ⊥)), x.IsAmalgamation (R := s.arrows) x_1
Tactic: rw [@existsUnique_iff_exists _ ⟨fun _ _ => _⟩]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊥) s
x : Presieve.FamilyOfElements (F ⋙ Functor.obj coyoneda (op c)) s.arrows
h : x.Compatible (R := s.arrows)
inl : ∃ (x_1 : (F ⋙ Functor.obj coyoneda (op c)).obj (op ⊥)), x.IsAmalgamation (R := s.arrows) x_1
⊢ ∃! t : (F ⋙ Functor.obj coyoneda (op c)).obj (op ⊥), x.IsAmalgamation (R := s.arrows) t
have rw : ∀ (x x_1 : (F ⋙ Functor.obj coyoneda (op c)).obj (op ⊥)), x = x_1
Tactic: rw [@existsUnique_iff_exists _ ⟨fun _ _ => _⟩]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊥) s
x : Presieve.FamilyOfElements (F ⋙ Functor.obj coyoneda (op c)) s.arrows
h : x.Compatible (R := s.arrows)
⊢ ∃ (x_1 : (F ⋙ Functor.obj coyoneda (op c)).obj (op ⊥)), x.IsAmalgamation (R := s.arrows) x_1
have inl : (U : TopologicalSpace.Opens (↑X : Type w)) → (hU : U ⟶ ⊥) → (hs : s.arrows hU) → IsTerminal.{v, u} (F.obj (op U))
Tactic: refine ⟨it.from _, fun U hU hs => IsTerminal.hom_ext ?_ _ _⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens (↑X : Type w)
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) U
this : IndiscreteTopology.{w} (↑X : Type w)
hne : U ≠ ⊥
⊢ Presieve.IsSheafFor (F ⋙ Functor.obj coyoneda (op c)) s.arrows
have h : s.arrows = ⊤
Tactic: convert! Presieve.isSheafFor_top (F ⋙ coyoneda.obj (@op C c))
-- Lean 4 proof step from Mathlib.Topology.Sheaves.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens (↑X : Type w)
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) U
this : IndiscreteTopology.{w} (↑X : Type w)
hne : U ≠ ⊥
⊢ s.arrows = ⊤
have h : s.arrows (𝟙 U)
Tactic: rw [Sieve.arrows_eq_top_iff, ← Sieve.id_mem_iff_eq_top]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.PUnit (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens (↑X : Type w)
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) U
this : IndiscreteTopology.{w} (↑X : Type w)
hne : U ≠ ⊥
⊢ s.arrows (𝟙 U)
have this₁ : U = ⊤
Tactic: have := U.eq_bot_or_top.resolve_left hne
-- Lean 4 proof step from Mathlib.Topology.Sheaves.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens (↑X : Type w)
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) U
this_1 : IndiscreteTopology.{w} (↑X : Type w)
hne : U ≠ ⊥
this : U = ⊤
⊢ s.arrows (𝟙 U)
have h : ∀ (s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤)
  (hs :
    Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤))
      ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊤) s)
  (hne : Ne.{w + 1} (α := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊥), s.arrows (𝟙 ⊤)
Tactic: subst this
Cleared hypotheses: U, s, hs, hne, this
-- Lean 4 proof step from Mathlib.Topology.Sheaves.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊤) s
hne : Ne.{w + 1} (α := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊥
⊢ s.arrows (𝟙 ⊤)
have h : ∀ (he : IsEmpty.{w + 1} (↑X : Type w)), s.arrows (𝟙 ⊤)
Tactic: obtain he | ⟨⟨x⟩⟩ := isEmpty_or_nonempty X
-- Lean 4 proof step from Mathlib.Topology.Sheaves.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊤) s
hne : Ne.{w + 1} (α := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊥
h : ∀ (he : IsEmpty.{w + 1} (↑X : Type w)), s.arrows (𝟙 ⊤)
⊢ s.arrows (𝟙 ⊤)
have h₁ : ∀ (x : (↑X : Type w)), s.arrows (𝟙 ⊤)
Tactic: obtain he | ⟨⟨x⟩⟩ := isEmpty_or_nonempty X
-- Lean 4 proof step from Mathlib.Topology.Sheaves.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊤) s
hne : Ne.{w + 1} (α := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊥
x : (↑X : Type w)
⊢ s.arrows (𝟙 ⊤)
have h : ∀ (U : TopologicalSpace.Opens (↑X : Type w)) (f : U ⟶ ⊤) (hf : s.arrows f) (hm : x ∈ U), s.arrows (𝟙 ⊤)
Tactic: obtain ⟨U, f, hf, hm⟩ := hs x _root_.trivial
-- Lean 4 proof step from Mathlib.Topology.Sheaves.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊤) s
hne : Ne.{w + 1} (α := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊥
x : (↑X : Type w)
U : TopologicalSpace.Opens (↑X : Type w)
f : U ⟶ ⊤
hf : s.arrows f
hm : x ∈ U
⊢ s.arrows (𝟙 ⊤)
have h : ∀ (f : Quiver.Hom (V := TopologicalSpace.Opens (↑X : Type w)) ⊥ ⊤) (hf : s.arrows f)
  (hm : Membership.mem (γ := TopologicalSpace.Opens (↑X : Type w)) ⊥ x), s.arrows (𝟙 ⊤)
Tactic: obtain rfl | rfl := U.eq_bot_or_top
Cleared hypotheses: U, f, hf, hm
-- Lean 4 proof step from Mathlib.Topology.Sheaves.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊤) s
hne : Ne.{w + 1} (α := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊥
x : (↑X : Type w)
U : TopologicalSpace.Opens (↑X : Type w)
f : U ⟶ ⊤
hf : s.arrows f
hm : x ∈ U
h :
  ∀ (f : Quiver.Hom (V := TopologicalSpace.Opens (↑X : Type w)) ⊥ ⊤) (hf : s.arrows f)
    (hm : Membership.mem (γ := TopologicalSpace.Opens (↑X : Type w)) ⊥ x), s.arrows (𝟙 ⊤)
⊢ s.arrows (𝟙 ⊤)
have h₁ : ∀ (f : Quiver.Hom (V := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊤) (hf : s.arrows f)
  (hm : Membership.mem (γ := TopologicalSpace.Opens (↑X : Type w)) ⊤ x), s.arrows (𝟙 ⊤)
Tactic: obtain rfl | rfl := U.eq_bot_or_top
Cleared hypotheses: U, f, hf, hm
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Points (goal)
Goal:
X : Type u
inst : TopologicalSpace X
U : Opens X
S : Sieve U
hS :
  ∀
    (Φ :
      ObjectProperty.FullSubcategory (C := Point (C := Opens X) (grothendieckTopology X))
        (pointsGrothendieckTopology X))
    (x : Φ.obj (P := pointsGrothendieckTopology X).fiber.obj U),
    ∃ (Y : Opens X) (g : Y ⟶ U) (_ : S.arrows g) (y : Φ.obj (P := pointsGrothendieckTopology X).fiber.obj Y),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := pointsGrothendieckTopology X).fiber.map g) :
            (a : (fun (X : Type u) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type u) ↦ X) (Φ.obj.fiber.obj U))
          y =
        x
x : X
hx : x ∈ U
⊢ ∃ (U_1 : Opens X) (f : U_1 ⟶ U), S.arrows f ∧ x ∈ U_1
have obtain : ∀ (V : Opens X) (f : V ⟶ U) (hf : S.arrows f) (hV : x ∈ V),
  (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (Point.fiber
                (ObjectProperty.FullSubcategory.obj (P := pointsGrothendieckTopology X)
                  (ObjectProperty.FullSubcategory.mk (P := pointsGrothendieckTopology X) (pointGrothendieckTopology x)
                    sorry)))
              f) :
          (a : (fun (X : Type u) ↦ X) ({ obj := pointGrothendieckTopology x, property := sorry }.obj.fiber.obj V)) →
            (fun (X : Type u) ↦ X) ({ obj := pointGrothendieckTopology x, property := sorry }.obj.fiber.obj U))
        { down := { down := hV } } =
      { down := { down := hx : PLift (x ∈ U) } : ULift.{u, 0} (PLift (x ∈ U)) } →
    ∃ (U_1 : Opens X) (f : U_1 ⟶ U), S.arrows f ∧ x ∈ U_1
Tactic: obtain ⟨V, f, hf, ⟨⟨hV⟩⟩, _⟩ := hS ⟨_, ⟨x⟩⟩ ⟨⟨hx⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Points (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
x_1 x_2 : Point (C := Opens X) (grothendieckTopology X)
x_3 x_4 : x_1 ⟶ x_2
⊢ x_3 = x_4
have h : ∀ (x : Opens X) (x_5 : x_2.fiber.obj x),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (x_3.hom.app x)).toFun x_5 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (x_4.hom.app x)).toFun x_5
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
P Q : Presheaf.{w, v, u} C X
f g : P ⟶ Q
w : ∀ (U : Opens (↑X : Type w)), Eq (α := P.obj (op U) ⟶ Q.obj (op U)) (f.app (op U)) (g.app (op U))
⊢ f = g
have app : f.app = g.app
Tactic: apply NatTrans.ext
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
P Q : Presheaf.{w, v, u} C X
f g : P ⟶ Q
w : ∀ (U : Opens (↑X : Type w)), Eq (α := P.obj (op U) ⟶ Q.obj (op U)) (f.app (op U)) (g.app (op U))
⊢ f.app = g.app
have app : ∀ (U : (Opens (↑X : Type w))ᵒᵖ), f.app U = g.app U
Tactic: ext U
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Presheaf (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
F : Presheaf.{w, v, u} C X
U V W : Opens (↑X : Type w)
e₁ : U ≤ V
e₂ : V ≤ W
x : ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (F.obj (op W))
⊢ restrictOpen (FC := FC) (CC := CC) (restrictOpen (FC := FC) (CC := CC) x V e₂) U e₁ =
    restrictOpen (FC := FC) (CC := CC) x U ⋯
have delta : Eq (α := ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (F.obj (op U)))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE e₁).op) : (a : CC (F.obj (op V))) → CC (F.obj (op U)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE e₂).op) :
            (a : CC (F.obj (op W))) → CC (F.obj (op V)))
          x :
        CC (F.obj (op V))) :
    CC (F.obj (op U)))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE sorry).op) : (a : CC (F.obj (op W))) → CC (F.obj (op U))) x :
    CC (F.obj (op U)))
Tactic: delta restrictOpen restrict
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Presheaf (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
F : Presheaf.{w, v, u} C X
U V W : Opens (↑X : Type w)
e₁ : U ≤ V
e₂ : V ≤ W
x : ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (F.obj (op W))
⊢ Eq (α := ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (F.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE e₁).op) : (a : CC (F.obj (op V))) → CC (F.obj (op U)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE e₂).op) :
              (a : CC (F.obj (op W))) → CC (F.obj (op V)))
            x :
          CC (F.obj (op V))) :
      CC (F.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) : (a : CC (F.obj (op W))) → CC (F.obj (op U)))
        x :
      CC (F.obj (op U)))
have rw : Eq (α := ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (F.obj (op U)))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map ((homOfLE e₂).op ≫ (homOfLE e₁).op)) :
        (a : CC (F.obj (op W))) → CC (F.obj (op U)))
      x :
    CC (F.obj (op U)))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE sorry).op) : (a : CC (F.obj (op W))) → CC (F.obj (op U))) x :
    CC (F.obj (op U)))
Tactic: rw [← ConcreteCategory.comp_apply, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Presheaf (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
F G : Presheaf.{w, v, u} C X
e : F ⟶ G
U V : Opens (↑X : Type w)
h : U ≤ V
x : ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (F.obj (op V))
⊢ Eq (α := CC (G.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (e.app (op U)) : (a : CC (F.obj (op U))) → CC (G.obj (op U)))
        (restrictOpen (FC := FC) (CC := CC) x U h) :
      CC (G.obj (op U)))
    (restrictOpen (FC := FC) (CC := CC)
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (e.app (op V)) : (a : CC (F.obj (op V))) → CC (G.obj (op V))) x) U
        h :
      ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (G.obj (op U)))
have delta : Eq (α := CC (G.obj (op U)))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (e.app (op U)) : (a : CC (F.obj (op U))) → CC (G.obj (op U)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE h).op) : (a : CC (F.obj (op V))) → CC (F.obj (op U)))
          x :
        CC (F.obj (op U))) :
    CC (G.obj (op U)))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map (homOfLE h).op) : (a : CC (G.obj (op V))) → CC (G.obj (op U)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (e.app (op V)) : (a : CC (F.obj (op V))) → CC (G.obj (op V))) x :
        CC (G.obj (op V))) :
    CC (G.obj (op U)))
Tactic: delta restrictOpen restrict