awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst_1 : IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)
U : X.Opens
hU : Membership.mem (α := ↥X) U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) : ↥X)
this_1 : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) = x
this : x ∈ U
⊢ X.presheaf.germ U x this ≫
      Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫
        Hom.appLE (Spec.map f) ⊤ ((Opens.map (Spec.map f).base).obj ⊤) ⋯ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f
have rw : X.presheaf.germ U x this ≫ Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫ Hom.app (Spec.map f) ⊤ ≫ (ΓSpecIso R).hom =
  X.presheaf.germ U x sorry ≫ f
Tactic: rw [← (Spec.map f).app_eq_appLE, ΓSpecIso_naturality, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst_1 : IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)
U : X.Opens
hU : Membership.mem (α := ↥X) U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) : ↥X)
this_1 : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) = x
this : x ∈ U
rw :
  X.presheaf.germ U x this ≫ Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫ Hom.app (Spec.map f) ⊤ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f
⊢ X.presheaf.germ U x this ≫
      Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫
        Hom.appLE (Spec.map f) ⊤ ((Opens.map (Spec.map f).base).obj ⊤) ⋯ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f
have rw₁ : X.presheaf.germ U x this ≫ Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫ Iso.hom (ΓSpecIso (X.presheaf.stalk x)) ≫ f =
  X.presheaf.germ U x sorry ≫ f
Tactic: rw [← (Spec.map f).app_eq_appLE, ΓSpecIso_naturality, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst_1 : IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)
U : X.Opens
hU : Membership.mem (α := ↥X) U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) : ↥X)
this_1 : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) = x
this : x ∈ U
rw :
  X.presheaf.germ U x this ≫ Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫ Hom.app (Spec.map f) ⊤ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f
rw₁ :
  X.presheaf.germ U x this ≫ Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫ Iso.hom (ΓSpecIso (X.presheaf.stalk x)) ≫ f =
    X.presheaf.germ U x ⋯ ≫ f
⊢ X.presheaf.germ U x this ≫
      Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫
        Hom.appLE (Spec.map f) ⊤ ((Opens.map (Spec.map f).base).obj ⊤) ⋯ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f
have rw₂ : X.presheaf.germ U x this ≫ f = X.presheaf.germ U x sorry ≫ f
Tactic: rw [← (Spec.map f).app_eq_appLE, ΓSpecIso_naturality, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X Y : Scheme
f_1 : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
x : ↥X
⊢ Inseparable ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u))) x
have rw : Inseparable x x
Tactic: rw [fromSpecStalk_closedPoint]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
x : ↥X
⊢ stalkClosedPointTo (X.fromSpecStalk x) = Iso.hom (X.presheaf.stalkCongr ⋯)
have refine : ∀ (U : TopologicalSpace.Opens ↥X)
  (hxU : Membership.mem (α := ↥X) U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥X)),
  X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u))) hxU ≫
      stalkClosedPointTo (X.fromSpecStalk x) =
    X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u))) hxU ≫
      Iso.hom (X.presheaf.stalkCongr sorry)
Tactic: refine TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
x : ↥X
U : TopologicalSpace.Opens ↥X
hxU : Membership.mem (α := ↥X) U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥X)
⊢ X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u))) hxU ≫
      stalkClosedPointTo (X.fromSpecStalk x) =
    X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u))) hxU ≫
      Iso.hom (X.presheaf.stalkCongr ⋯)
have simp : X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u))) hxU ≫
    stalkClosedPointTo (X.fromSpecStalk x) =
  X.presheaf.germ U x sorry
Tactic: simp only [TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (hypothesis)
Goal:
X : Scheme
x : ↥X
U : TopologicalSpace.Opens ↥X
hxU : Membership.mem (α := ↥X) U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥X)
⊢ X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u))) hxU ≫
      stalkClosedPointTo (X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯
have this : X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x
Tactic: have : X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x := by simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
⊢ CategoryStruct.comp (Y := Spec (X.presheaf.stalk (f (closedPoint (↑R : Type u))))) (Spec.map (stalkClosedPointTo f))
      (X.fromSpecStalk (f (closedPoint (↑R : Type u)))) =
    f
have obtain : ∀ (U : TopologicalSpace.Opens ↥X) (hU : U ∈ X.affineOpens)
  (hxU : Membership.mem (α := ↥X) (↑U : Set ↥X) (f (closedPoint (↑R : Type u)) : ↥X)),
  CategoryStruct.comp (Y := Spec (X.presheaf.stalk (f (closedPoint (↑R : Type u))))) (Spec.map (stalkClosedPointTo f))
      (X.fromSpecStalk (f (closedPoint (↑R : Type u)))) =
    f
Tactic: obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open
    (Set.mem_univ (f (closedPoint R))) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (hypothesis)
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : Membership.mem (α := ↥X) (↑U : Set ↥X) (f (closedPoint (↑R : Type u)) : ↥X)
⊢ CategoryStruct.comp (Y := Spec (X.presheaf.stalk (f (closedPoint (↑R : Type u))))) (Spec.map (stalkClosedPointTo f))
      (X.fromSpecStalk (f (closedPoint (↑R : Type u)))) =
    f
have this : Spec.map (Hom.appLE f U ⊤ sorry) ≫ IsAffineOpen.fromSpec hU = IsAffineOpen.fromSpec sorry ≫ f
Tactic: have := IsAffineOpen.SpecMap_appLE_fromSpec f hU (isAffineOpen_top _)
    (preimage_eq_top_of_closedPoint_mem f hxU).ge
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (hypothesis)
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : Membership.mem (α := ↥X) (↑U : Set ↥X) (f (closedPoint (↑R : Type u)) : ↥X)
this : Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = IsAffineOpen.fromSpec ⋯ ≫ f
⊢ CategoryStruct.comp (Y := Spec (X.presheaf.stalk (f (closedPoint (↑R : Type u))))) (Spec.map (stalkClosedPointTo f))
      (X.fromSpecStalk (f (closedPoint (↑R : Type u)))) =
    f
have this₁ : Spec.map (ΓSpecIso R).hom ≫ Spec.map (Hom.appLE f U ⊤ sorry) ≫ IsAffineOpen.fromSpec hU = f
Tactic: rw [IsAffineOpen.fromSpec_top, Iso.eq_inv_comp, isoSpec_Spec_hom] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : Membership.mem (α := ↥X) (↑U : Set ↥X) (f (closedPoint (↑R : Type u)) : ↥X)
this : Spec.map (ΓSpecIso R).hom ≫ Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = f
⊢ CategoryStruct.comp (Y := Spec (X.presheaf.stalk (f (closedPoint (↑R : Type u))))) (Spec.map (stalkClosedPointTo f))
      (X.fromSpecStalk (f (closedPoint (↑R : Type u)))) =
    f
have rw : Spec.map (Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (Iso.op (eqToIso sorry)) ≪≫ ΓSpecIso R).hom) ≫
    IsAffineOpen.fromSpec hU =
  f
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc,
    germ_stalkClosedPointTo]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f₁ f₂ :
  (x : ↥X) ×
    { f : X.presheaf.stalk x ⟶ R //
      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }
h₁ :
  f₁.fst (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }) =
    f₂.fst (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
⊢ Inseparable
    (f₁.fst (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }))
    (f₂.fst (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }))
have rw : Inseparable
  (f₂.fst (β := fun (x : ↥X) ↦
    { f : X.presheaf.stalk x ⟶ R //
      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }))
  (f₂.fst (β := fun (x : ↥X) ↦
    { f : X.presheaf.stalk x ⟶ R //
      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }))
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
R : CommRingCat
f₁ f₂ :
  (x : ↥X) ×
    { f : X.presheaf.stalk x ⟶ R //
      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }
⊢ f₁ = f₂ ↔
    ∃ (h₁ :
      f₁.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }) =
        f₂.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })),
      (↑(f₁.snd (β := fun (x : ↥X) ↦
              { f : X.presheaf.stalk x ⟶ R //
                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
          X.presheaf.stalk f₁.fst ⟶ R) =
        Iso.hom (X.presheaf.stalkCongr ⋯) ≫
          (↑(f₂.snd (β := fun (x : ↥X) ↦
                { f : X.presheaf.stalk x ⟶ R //
                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
            X.presheaf.stalk f₂.fst ⟶ R)
have mp : f₁ = f₂ →
  ∃ (h₁ :
    f₁.fst (β := fun (x : ↥X) ↦
        { f : X.presheaf.stalk x ⟶ R //
          IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }) =
      f₂.fst (β := fun (x : ↥X) ↦
        { f : X.presheaf.stalk x ⟶ R //
          IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })),
    (↑(f₁.snd (β := fun (x : ↥X) ↦
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
        X.presheaf.stalk f₁.fst ⟶ R) =
      Iso.hom (X.presheaf.stalkCongr sorry) ≫
        (↑(f₂.snd (β := fun (x : ↥X) ↦
              { f : X.presheaf.stalk x ⟶ R //
                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
          X.presheaf.stalk f₂.fst ⟶ R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
R : CommRingCat
f₁ f₂ :
  (x : ↥X) ×
    { f : X.presheaf.stalk x ⟶ R //
      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }
mp :
  f₁ = f₂ →
    ∃ (h₁ :
      f₁.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }) =
        f₂.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })),
      (↑(f₁.snd (β := fun (x : ↥X) ↦
              { f : X.presheaf.stalk x ⟶ R //
                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
          X.presheaf.stalk f₁.fst ⟶ R) =
        Iso.hom (X.presheaf.stalkCongr ⋯) ≫
          (↑(f₂.snd (β := fun (x : ↥X) ↦
                { f : X.presheaf.stalk x ⟶ R //
                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
            X.presheaf.stalk f₂.fst ⟶ R)
⊢ f₁ = f₂ ↔
    ∃ (h₁ :
      f₁.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }) =
        f₂.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })),
      (↑(f₁.snd (β := fun (x : ↥X) ↦
              { f : X.presheaf.stalk x ⟶ R //
                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
          X.presheaf.stalk f₁.fst ⟶ R) =
        Iso.hom (X.presheaf.stalkCongr ⋯) ≫
          (↑(f₂.snd (β := fun (x : ↥X) ↦
                { f : X.presheaf.stalk x ⟶ R //
                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
            X.presheaf.stalk f₂.fst ⟶ R)
have mpr : (∃ (h₁ :
    f₁.fst (β := fun (x : ↥X) ↦
        { f : X.presheaf.stalk x ⟶ R //
          IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }) =
      f₂.fst (β := fun (x : ↥X) ↦
        { f : X.presheaf.stalk x ⟶ R //
          IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })),
    (↑(f₁.snd (β := fun (x : ↥X) ↦
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
        X.presheaf.stalk f₁.fst ⟶ R) =
      Iso.hom (X.presheaf.stalkCongr sorry) ≫
        (↑(f₂.snd (β := fun (x : ↥X) ↦
              { f : X.presheaf.stalk x ⟶ R //
                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
          X.presheaf.stalk f₂.fst ⟶ R)) →
  f₁ = f₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
P : (↑(PrimeSpectrum.Top R) : Type u)
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
a b : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    a
hb :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    b
x : ↥U
⊢ ∃ (V : Opens (↑(PrimeSpectrum.Top R) : Type u)) (_ : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V) (i : V ⟶ U),
    PrelocalPredicate.pred (T := Localizations M) (isFractionPrelocal R M) (U := V) fun (x : ↥V) ↦
      (a + b) ((i : (a : ↥V) → ↥U) x)
have obtain : ∀ (Va : Opens (↑(PrimeSpectrum.Top R) : Type u)) (ma : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Va) (ia : Va ⟶ U)
  (ra : M) (sa : R)
  (wa :
    ∀ (x : ↥Va),
      ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
        Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
          ((fun (x : ↥Va) ↦
              (a ((ia : (a : ↥Va) → ↥U) x) :
                Localizations (R := R) M (↑((ia : (a : ↥Va) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
            x)
          (LocalizedModule.mk ra
            (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sa
              hs))),
  ∃ (V : Opens (↑(PrimeSpectrum.Top R) : Type u)) (_ : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V) (i : V ⟶ U),
    PrelocalPredicate.pred (T := Localizations M) (isFractionPrelocal R M) (U := V) fun (x : ↥V) ↦
      (a + b) ((i : (a : ↥V) → ↥U) x)
Tactic: obtain ⟨Va, ma, ia, ra, sa, wa⟩ := ha x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
P : (↑(PrimeSpectrum.Top R) : Type u)
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
a b : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    a
hb :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    b
x : ↥U
Va : Opens (↑(PrimeSpectrum.Top R) : Type u)
ma : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Va
ia : Va ⟶ U
ra : M
sa : R
wa :
  ∀ (x : ↥Va),
    ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Va) ↦
            (a ((ia : (a : ↥Va) → ↥U) x) :
              Localizations (R := R) M (↑((ia : (a : ↥Va) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk ra
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sa hs))
⊢ ∃ (V : Opens (↑(PrimeSpectrum.Top R) : Type u)) (_ : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V) (i : V ⟶ U),
    PrelocalPredicate.pred (T := Localizations M) (isFractionPrelocal R M) (U := V) fun (x : ↥V) ↦
      (a + b) ((i : (a : ↥V) → ↥U) x)
have obtain : ∀ (Vb : Opens (↑(PrimeSpectrum.Top R) : Type u)) (mb : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Vb) (ib : Vb ⟶ U)
  (rb : M) (sb : R)
  (wb :
    ∀ (x : ↥Vb),
      ∃ (hs : sb ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
        Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
          ((fun (x : ↥Vb) ↦
              (b ((ib : (a : ↥Vb) → ↥U) x) :
                Localizations (R := R) M (↑((ib : (a : ↥Vb) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
            x)
          (LocalizedModule.mk rb
            (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sb
              hs))),
  ∃ (V : Opens (↑(PrimeSpectrum.Top R) : Type u)) (_ : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V) (i : V ⟶ U),
    PrelocalPredicate.pred (T := Localizations M) (isFractionPrelocal R M) (U := V) fun (x : ↥V) ↦
      (a + b) ((i : (a : ↥V) → ↥U) x)
Tactic: obtain ⟨Vb, mb, ib, rb, sb, wb⟩ := hb x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
P : (↑(PrimeSpectrum.Top R) : Type u)
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
a b : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    a
hb :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    b
x : ↥U
Va : Opens (↑(PrimeSpectrum.Top R) : Type u)
ma : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Va
ia : Va ⟶ U
ra : M
sa : R
wa :
  ∀ (x : ↥Va),
    ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Va) ↦
            (a ((ia : (a : ↥Va) → ↥U) x) :
              Localizations (R := R) M (↑((ia : (a : ↥Va) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk ra
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sa hs))
Vb : Opens (↑(PrimeSpectrum.Top R) : Type u)
mb : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Vb
ib : Vb ⟶ U
rb : M
sb : R
wb :
  ∀ (x : ↥Vb),
    ∃ (hs : sb ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Vb) ↦
            (b ((ib : (a : ↥Vb) → ↥U) x) :
              Localizations (R := R) M (↑((ib : (a : ↥Vb) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk rb
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sb hs))
⊢ ∃ (V : Opens (↑(PrimeSpectrum.Top R) : Type u)) (_ : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V) (i : V ⟶ U),
    PrelocalPredicate.pred (T := Localizations M) (isFractionPrelocal R M) (U := V) fun (x : ↥V) ↦
      (a + b) ((i : (a : ↥V) → ↥U) x)
have refine : ∀ (x : ↥(Va ⊓ Vb)),
  ∃ (hs : sa * sb ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
    Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
      ((fun (x : ↥(Va ⊓ Vb)) ↦ (a + b) ((Va.infLELeft Vb ≫ ia : (a : ↥(Va ⊓ Vb)) → ↥U) x)) x)
      (LocalizedModule.mk (sb • ra + sa • rb)
        (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) (sa * sb)
          hs))
Tactic: refine ⟨Va ⊓ Vb, ⟨ma, mb⟩, Opens.infLELeft _ _ ≫ ia, sb • ra + sa • rb, sa * sb, fun x ↦ ?_⟩