awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U V W : (Opens (↑X : Type w))ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ Eq (α := CommRingCat.of (Localization (G.obj U)) ⟶ CommRingCat.of (Localization (G.obj W)))
    (ConcreteCategory.ofHom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
      CommRingCat.carrier)
      (IsLocalization.map (T := G.obj W) (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map i ≫ F.map j)) ⋯))
    (CategoryStruct.comp (Y := CommRingCat.of (Localization (G.obj V)))
      (ConcreteCategory.ofHom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
        CommRingCat.carrier) (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) ⋯))
      (ConcreteCategory.ofHom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
        CommRingCat.carrier) (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) ⋯)))
have hf : Eq (α :=
  (↑(CommRingCat.of (Localization (G.obj U))) : Type w) →+* (↑(CommRingCat.of (Localization (G.obj W))) : Type w))
  (CommRingCat.Hom.hom
    (ConcreteCategory.ofHom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
      CommRingCat.carrier)
      (IsLocalization.map (T := G.obj W) (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map i ≫ F.map j)) sorry)))
  (CommRingCat.Hom.hom
    (CategoryStruct.comp (Y := CommRingCat.of (Localization (G.obj V)))
      (ConcreteCategory.ofHom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
        CommRingCat.carrier) (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) sorry))
      (ConcreteCategory.ofHom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
        CommRingCat.carrier) (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) sorry))))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U V W : (Opens (↑X : Type w))ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ Eq (α :=
    (↑(CommRingCat.of (Localization (G.obj U))) : Type w) →+* (↑(CommRingCat.of (Localization (G.obj W))) : Type w))
    (CommRingCat.Hom.hom
      (ConcreteCategory.ofHom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
        CommRingCat.carrier)
        (IsLocalization.map (T := G.obj W) (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map i ≫ F.map j)) ⋯)))
    (CommRingCat.Hom.hom
      (CategoryStruct.comp (Y := CommRingCat.of (Localization (G.obj V)))
        (ConcreteCategory.ofHom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
          CommRingCat.carrier) (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) ⋯))
        (ConcreteCategory.ofHom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
          CommRingCat.carrier) (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) ⋯))))
have hf : Eq (α := Localization (G.obj U) →+* Localization (G.obj W))
  (IsLocalization.map (T := G.obj W) (Localization (G.obj W))
    ((CommRingCat.Hom.hom (F.map j)).comp (CommRingCat.Hom.hom (F.map i))) sorry)
  (@RingHom.comp _ (Localization (G.obj V)) _ _ Semiring.toNonAssocSemiring _
    (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) sorry)
    (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) sorry))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U V W : (Opens (↑X : Type w))ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ Eq (α := Localization (G.obj U) →+* Localization (G.obj W))
    (IsLocalization.map (T := G.obj W) (Localization (G.obj W))
      ((CommRingCat.Hom.hom (F.map j)).comp (CommRingCat.Hom.hom (F.map i))) ⋯)
    (@RingHom.comp _ (Localization (G.obj V)) _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) ⋯)
      (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) ⋯))
have hf : Eq (α := Localization (G.obj U) →+* Localization (G.obj W))
  (IsLocalization.map (T := G.obj W) (Localization (G.obj W))
    ((CommRingCat.Hom.hom (F.map j)).comp (CommRingCat.Hom.hom (F.map i))) sorry)
  (IsLocalization.map (M := G.obj U) (T := G.obj W) (Localization (G.obj W))
    ((CommRingCat.Hom.hom (F.map j)).comp (CommRingCat.Hom.hom (F.map i))) sorry)
Tactic: rw [IsLocalization.map_comp_map]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
S : (x : (↑X : Type w)) → Submonoid (↑(F.stalk x) : Type w)
U V : (Opens (↑X : Type w))ᵒᵖ
i : U ⟶ V
s : (↑(F.obj U) : Type w)
hs :
  Membership.mem (γ := Submonoid (↑(F.obj U) : Type w))
    (⨅ (x : ↥(unop U)),
      Submonoid.comap (F := (↑(F.obj (op (unop U))) : Type w) →+* (↑(F.stalk (↑x : (↑X : Type w))) : Type w))
        (CommRingCat.Hom.hom (F.germ (unop U) (↑x : (↑X : Type w)) ⋯)) (S (↑x : (↑X : Type w))))
    s
⊢ Membership.mem (γ := Submonoid (↑(F.obj U) : Type w))
    (Submonoid.comap (CommRingCat.Hom.hom (F.map i))
      (⨅ (x : ↥(unop V)),
        Submonoid.comap (F := (↑(F.obj (op (unop V))) : Type w) →+* (↑(F.stalk (↑x : (↑X : Type w))) : Type w))
          (CommRingCat.Hom.hom (F.germ (unop V) (↑x : (↑X : Type w)) ⋯)) (S (↑x : (↑X : Type w)))))
    s
have simp : ∀
  (hs :
    ∀ (i : ↥(unop U)),
      Membership.mem (α := (↑(F.stalk (↑i : (↑X : Type w))) : Type w)) (γ :=
        Submonoid (↑(F.stalk (↑i : (↑X : Type w))) : Type w)) (S (↑i : (↑X : Type w)))
        ((CommRingCat.Hom.hom (F.germ (unop U) (↑i : (↑X : Type w)) sorry) :
              (a : (↑(F.obj U) : Type w)) → (↑(F.stalk (↑i : (↑X : Type w))) : Type w))
            s :
          (↑(F.stalk (↑i : (↑X : Type w))) : Type w)))
  (i_1 : ↥(unop V)),
  Membership.mem (α := (↑(F.stalk (↑i_1 : (↑X : Type w))) : Type w)) (γ :=
    Submonoid (↑(F.stalk (↑i_1 : (↑X : Type w))) : Type w)) (S (↑i_1 : (↑X : Type w)))
    ((CommRingCat.Hom.hom (F.germ (unop V) (↑i_1 : (↑X : Type w)) sorry) :
          (a : (↑(F.obj V) : Type w)) → (↑(F.stalk (↑i_1 : (↑X : Type w))) : Type w))
        ((CommRingCat.Hom.hom (F.map i) : (a : (↑(F.obj U) : Type w)) → (↑(F.obj V) : Type w)) s :
          (↑(F.obj V) : Type w)) :
      (↑(F.stalk (↑i_1 : (↑X : Type w))) : Type w))
Tactic: simp only [Submonoid.mem_comap, Submonoid.mem_iInf] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
S : (x : (↑X : Type w)) → Submonoid (↑(F.stalk x) : Type w)
U V : (Opens (↑X : Type w))ᵒᵖ
i : U ⟶ V
s : (↑(F.obj U) : Type w)
hs :
  ∀ (i : ↥(unop U)),
    Membership.mem (α := (↑(F.stalk (↑i : (↑X : Type w))) : Type w)) (γ :=
      Submonoid (↑(F.stalk (↑i : (↑X : Type w))) : Type w)) (S (↑i : (↑X : Type w)))
      ((CommRingCat.Hom.hom (F.germ (unop U) (↑i : (↑X : Type w)) ⋯) :
            (a : (↑(F.obj U) : Type w)) → (↑(F.stalk (↑i : (↑X : Type w))) : Type w))
          s :
        (↑(F.stalk (↑i : (↑X : Type w))) : Type w))
x : ↥(unop V)
⊢ Membership.mem (α := (↑(F.stalk (↑x : (↑X : Type w))) : Type w)) (γ :=
    Submonoid (↑(F.stalk (↑x : (↑X : Type w))) : Type w)) (S (↑x : (↑X : Type w)))
    ((CommRingCat.Hom.hom (F.germ (unop V) (↑x : (↑X : Type w)) ⋯) :
          (a : (↑(F.obj V) : Type w)) → (↑(F.stalk (↑x : (↑X : Type w))) : Type w))
        ((CommRingCat.Hom.hom (F.map i) : (a : (↑(F.obj U) : Type w)) → (↑(F.obj V) : Type w)) s :
          (↑(F.obj V) : Type w)) :
      (↑(F.stalk (↑x : (↑X : Type w))) : Type w))
have change : Membership.mem (α := (↑(F.stalk (↑x : (↑X : Type w))) : Type w)) (γ :=
  Submonoid (↑(F.stalk (↑x : (↑X : Type w))) : Type w)) (S (↑x : (↑X : Type w)))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
          CommRingCat.carrier) (Y := F.stalk (↑x : (↑X : Type w)))
          (F.map i.unop.op ≫ F.germ (unop V) (↑x : (↑X : Type w)) sorry) :
        (a : (↑(F.obj (op (unop U))) : Type w)) → (↑(F.stalk (↑x : (↑X : Type w))) : Type w))
      s :
    (↑(F.stalk (↑x : (↑X : Type w))) : Type w))
Tactic: change (F.map i.unop.op ≫ F.germ V.unop x.1 x.2) s ∈ _
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
S : (x : (↑X : Type w)) → Submonoid (↑(F.stalk x) : Type w)
U V : (Opens (↑X : Type w))ᵒᵖ
i : U ⟶ V
s : (↑(F.obj U) : Type w)
hs :
  ∀ (i : ↥(unop U)),
    Membership.mem (α := (↑(F.stalk (↑i : (↑X : Type w))) : Type w)) (γ :=
      Submonoid (↑(F.stalk (↑i : (↑X : Type w))) : Type w)) (S (↑i : (↑X : Type w)))
      ((CommRingCat.Hom.hom (F.germ (unop U) (↑i : (↑X : Type w)) ⋯) :
            (a : (↑(F.obj U) : Type w)) → (↑(F.stalk (↑i : (↑X : Type w))) : Type w))
          s :
        (↑(F.stalk (↑i : (↑X : Type w))) : Type w))
x : ↥(unop V)
⊢ Membership.mem (α := (↑(F.stalk (↑x : (↑X : Type w))) : Type w)) (γ :=
    Submonoid (↑(F.stalk (↑x : (↑X : Type w))) : Type w)) (S (↑x : (↑X : Type w)))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
            CommRingCat.carrier) (Y := F.stalk (↑x : (↑X : Type w)))
            (F.map i.unop.op ≫ F.germ (unop V) (↑x : (↑X : Type w)) ⋯) :
          (a : (↑(F.obj (op (unop U))) : Type w)) → (↑(F.stalk (↑x : (↑X : Type w))) : Type w))
        s :
      (↑(F.stalk (↑x : (↑X : Type w))) : Type w))
have rw : Membership.mem (α := (↑(F.stalk (↑x : (↑X : Type w))) : Type w)) (γ :=
  Submonoid (↑(F.stalk (↑x : (↑X : Type w))) : Type w)) (S (↑x : (↑X : Type w)))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
          CommRingCat.carrier) (Y := F.stalk (↑x : (↑X : Type w))) (F.germ (unop U) (↑x : (↑X : Type w)) sorry) :
        (a : (↑(F.obj (op (unop U))) : Type w)) → (↑(F.stalk (↑x : (↑X : Type w))) : Type w))
      s :
    (↑(F.stalk (↑x : (↑X : Type w))) : Type w))
Tactic: rw [F.germ_res]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F_1 : Presheaf CommRingCat X
G : F_1.SubmonoidPresheaf
F : Sheaf CommRingCat X
⊢ Mono F.presheaf.toTotalQuotientPresheaf
have inst : ∀ (X_1 : (Opens (↑X : Type w))ᵒᵖ), Mono (F.presheaf.toTotalQuotientPresheaf.app X_1)
Tactic: apply +allowSynthFailures NatTrans.mono_of_mono_app
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F_1 : Presheaf CommRingCat X
G : F_1.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens (↑X : Type w))ᵒᵖ
⊢ Mono (F.presheaf.toTotalQuotientPresheaf.app U)
have inst : Function.Injective (α := (↑(F.presheaf.obj U) : Type w)) (β := (↑(F.presheaf.totalQuotientPresheaf.obj U) : Type w))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
        CommRingCat.carrier) (F.presheaf.toTotalQuotientPresheaf.app U)) :
    (a : (↑(F.presheaf.obj U) : Type w)) → (↑(F.presheaf.totalQuotientPresheaf.obj U) : Type w))
Tactic: apply ConcreteCategory.mono_of_injective
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F_1 : Presheaf CommRingCat X
G : F_1.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens (↑X : Type w))ᵒᵖ
⊢ Function.Injective (α := (↑(F.presheaf.obj U) : Type w)) (β := (↑(F.presheaf.totalQuotientPresheaf.obj U) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
          CommRingCat.carrier) (F.presheaf.toTotalQuotientPresheaf.app U)) :
      (a : (↑(F.presheaf.obj U) : Type w)) → (↑(F.presheaf.totalQuotientPresheaf.obj U) : Type w))
have inst : Function.Injective (α := (↑(F.presheaf.obj U) : Type w)) (β := (↑(F.presheaf.totalQuotientPresheaf.obj U) : Type w))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
        CommRingCat.carrier) (X := F.presheaf.obj U) (Y := F.presheaf.totalQuotientPresheaf.obj U)
        (CommRingCat.ofHom
          (algebraMap (↑(F.presheaf.obj U) : Type w)
            (Localization (M := (↑(F.presheaf.obj U) : Type w))
              (⨅ (x : ↥(unop U)),
                Submonoid.comap (F :=
                  (↑(F.presheaf.obj U) : Type w) →+* (↑(F.presheaf.stalk (↑x : (↑X : Type w))) : Type w))
                  (CommRingCat.Hom.hom (F.presheaf.germ (unop U) (↑x : (↑X : Type w)) sorry))
                  (↑(F.presheaf.stalk (↑x : (↑X : Type w))) : Type w)⁰))))) :
    (a : (↑(F.presheaf.obj U) : Type w)) → (↑(F.presheaf.totalQuotientPresheaf.obj U) : Type w))
Tactic: dsimp [toTotalQuotientPresheaf]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F_1 : Presheaf CommRingCat X
G : F_1.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens (↑X : Type w))ᵒᵖ
m : Submonoid (↑(F.presheaf.obj U) : Type w) :=
  (F.presheaf.submonoidPresheafOfStalk fun (x : (↑X : Type w)) ↦ (↑(F.presheaf.stalk x) : Type w)⁰).obj U
⊢ Function.Injective (α := (↑(F.presheaf.obj U) : Type w)) (β := (↑(F.presheaf.totalQuotientPresheaf.obj U) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
          CommRingCat.carrier) (X := F.presheaf.obj U) (Y := F.presheaf.totalQuotientPresheaf.obj U)
          (CommRingCat.ofHom
            (algebraMap (↑(F.presheaf.obj U) : Type w)
              (Localization (M := (↑(F.presheaf.obj U) : Type w))
                (⨅ (x : ↥(unop U)),
                  Submonoid.comap (F :=
                    (↑(F.presheaf.obj U) : Type w) →+* (↑(F.presheaf.stalk (↑x : (↑X : Type w))) : Type w))
                    (CommRingCat.Hom.hom (F.presheaf.germ (unop U) (↑x : (↑X : Type w)) ⋯))
                    (↑(F.presheaf.stalk (↑x : (↑X : Type w))) : Type w)⁰))))) :
      (a : (↑(F.presheaf.obj U) : Type w)) → (↑(F.presheaf.totalQuotientPresheaf.obj U) : Type w))
have inst : Function.Injective.{w + 1, w + 1} (α := (↑(F.presheaf.obj U) : Type w)) (β := Localization m)
  (⇑(algebraMap (↑(F.presheaf.obj U) : Type w) (Localization m)) :
    (a : (↑(F.presheaf.obj U) : Type w)) → Localization m)
Tactic: change Function.Injective (algebraMap _ (Localization m))
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F_1 : Presheaf CommRingCat X
G : F_1.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens (↑X : Type w))ᵒᵖ
m : Submonoid (↑(F.presheaf.obj U) : Type w) :=
  (F.presheaf.submonoidPresheafOfStalk fun (x : (↑X : Type w)) ↦ (↑(F.presheaf.stalk x) : Type w)⁰).obj U
⊢ Function.Injective.{w + 1, w + 1} (α := (↑(F.presheaf.obj U) : Type w)) (β := Localization m)
    (⇑(algebraMap (↑(F.presheaf.obj U) : Type w) (Localization m)) :
      (a : (↑(F.presheaf.obj U) : Type w)) → Localization m)
have inst : m ≤ (↑(F.presheaf.obj U) : Type w)⁰
Tactic: refine IsLocalization.injective (M := m) (S := Localization m) ?_
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F_1 : Presheaf CommRingCat X
G : F_1.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens (↑X : Type w))ᵒᵖ
m : Submonoid (↑(F.presheaf.obj U) : Type w) :=
  (F.presheaf.submonoidPresheafOfStalk fun (x : (↑X : Type w)) ↦ (↑(F.presheaf.stalk x) : Type w)⁰).obj U
⊢ m ≤ (↑(F.presheaf.obj U) : Type w)⁰
have inst : m ≤ nonZeroDivisorsRight (↑(F.presheaf.obj U) : Type w)
Tactic: rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F_1 : Presheaf CommRingCat X
G : F_1.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens (↑X : Type w))ᵒᵖ
m : Submonoid (↑(F.presheaf.obj U) : Type w) :=
  (F.presheaf.submonoidPresheafOfStalk fun (x : (↑X : Type w)) ↦ (↑(F.presheaf.stalk x) : Type w)⁰).obj U
s : (↑(F.presheaf.obj U) : Type w)
hs : s ∈ m
t : (↑(F.presheaf.obj U) : Type w)
e : t * s = 0
⊢ t = 0
have inst : ∀ (x : (↑X : Type w)) (hx : x ∈ unop U),
  Eq (α := (↑(F.presheaf.stalk x) : Type w))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
            CommRingCat.carrier) (Y := F.presheaf.stalk x) (F.presheaf.germ (unop U) x hx) :
          (a : (↑(F.presheaf.obj (op (unop U))) : Type w)) → (↑(F.presheaf.stalk x) : Type w))
        t :
      (↑(F.presheaf.stalk x) : Type w))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
            CommRingCat.carrier) (Y := F.presheaf.stalk x) (F.presheaf.germ (unop U) x hx) :
          (a : (↑(F.presheaf.obj (op (unop U))) : Type w)) → (↑(F.presheaf.stalk x) : Type w))
        0 :
      (↑(F.presheaf.stalk x) : Type w))
Tactic: apply section_ext F (unop U)
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F_1 : Presheaf CommRingCat X
G : F_1.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens (↑X : Type w))ᵒᵖ
m : Submonoid (↑(F.presheaf.obj U) : Type w) :=
  (F.presheaf.submonoidPresheafOfStalk fun (x : (↑X : Type w)) ↦ (↑(F.presheaf.stalk x) : Type w)⁰).obj U
s : (↑(F.presheaf.obj U) : Type w)
hs : s ∈ m
t : (↑(F.presheaf.obj U) : Type w)
e : t * s = 0
x : (↑X : Type w)
hx : x ∈ unop U
⊢ Eq (α := (↑(F.presheaf.stalk x) : Type w))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
            CommRingCat.carrier) (Y := F.presheaf.stalk x) (F.presheaf.germ (unop U) x hx) :
          (a : (↑(F.presheaf.obj (op (unop U))) : Type w)) → (↑(F.presheaf.stalk x) : Type w))
        t :
      (↑(F.presheaf.stalk x) : Type w))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
            CommRingCat.carrier) (Y := F.presheaf.stalk x) (F.presheaf.germ (unop U) x hx) :
          (a : (↑(F.presheaf.obj (op (unop U))) : Type w)) → (↑(F.presheaf.stalk x) : Type w))
        0 :
      (↑(F.presheaf.stalk x) : Type w))
have inst : Eq (α := (↑(F.presheaf.stalk x) : Type w))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
          CommRingCat.carrier) (Y := F.presheaf.stalk x) (F.presheaf.germ (unop U) x hx) :
        (a : (↑(F.presheaf.obj (op (unop U))) : Type w)) → (↑(F.presheaf.stalk x) : Type w))
      t :
    (↑(F.presheaf.stalk x) : Type w))
  (0 : (↑(F.presheaf.stalk x) : Type w))
Tactic: rw [map_zero]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F_1 : Presheaf CommRingCat X
G : F_1.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens (↑X : Type w))ᵒᵖ
m : Submonoid (↑(F.presheaf.obj U) : Type w) :=
  (F.presheaf.submonoidPresheafOfStalk fun (x : (↑X : Type w)) ↦ (↑(F.presheaf.stalk x) : Type w)⁰).obj U
s : (↑(F.presheaf.obj U) : Type w)
hs : s ∈ m
t : (↑(F.presheaf.obj U) : Type w)
e : t * s = 0
x : (↑X : Type w)
hx : x ∈ unop U
⊢ Eq (α := (↑(F.presheaf.stalk x) : Type w))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
            CommRingCat.carrier) (Y := F.presheaf.stalk x) (F.presheaf.germ (unop U) x hx) :
          (a : (↑(F.presheaf.obj (op (unop U))) : Type w)) → (↑(F.presheaf.stalk x) : Type w))
        t :
      (↑(F.presheaf.stalk x) : Type w))
    (0 : (↑(F.presheaf.stalk x) : Type w))
have inst : HMul.hMul (α :=
    (↑(F.presheaf.stalk (↑(Subtype.mk (p := fun (x : (↑X : Type w)) ↦ x ∈ unop U) x hx) : (↑X : Type w))) : Type w))
    (β :=
    (↑(F.presheaf.stalk (↑(Subtype.mk (p := fun (x : (↑X : Type w)) ↦ x ∈ unop U) x hx) : (↑X : Type w))) : Type w))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
            CommRingCat.carrier) (Y := F.presheaf.stalk x) (F.presheaf.germ (unop U) x hx) :
          (a : (↑(F.presheaf.obj (op (unop U))) : Type w)) → (↑(F.presheaf.stalk x) : Type w))
        t :
      (↑(F.presheaf.stalk x) : Type w))
    ((CommRingCat.Hom.hom
            (F.presheaf.germ (unop U) (↑(Subtype.mk (p := fun (x : (↑X : Type w)) ↦ x ∈ unop U) x hx) : (↑X : Type w))
              sorry) :
          (a : (↑(F.presheaf.obj U) : Type w)) → (↑(F.presheaf.stalk (↑⟨x, hx⟩ : (↑X : Type w))) : Type w))
        s :
      (↑(F.presheaf.stalk (↑(Subtype.mk (p := fun (x : (↑X : Type w)) ↦ x ∈ unop U) x hx) : (↑X : Type w))) : Type w)) =
  0
Tactic: apply (Submonoid.mem_iInf.mp hs ⟨x, hx⟩).2
-- Lean 4 proof step from Mathlib.Topology.Sheaves.CommRingCat (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F_1 : Presheaf CommRingCat X
G : F_1.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens (↑X : Type w))ᵒᵖ
m : Submonoid (↑(F.presheaf.obj U) : Type w) :=
  (F.presheaf.submonoidPresheafOfStalk fun (x : (↑X : Type w)) ↦ (↑(F.presheaf.stalk x) : Type w)⁰).obj U
s : (↑(F.presheaf.obj U) : Type w)
hs : s ∈ m
t : (↑(F.presheaf.obj U) : Type w)
e : t * s = 0
x : (↑X : Type w)
hx : x ∈ unop U
⊢ HMul.hMul (α :=
      (↑(F.presheaf.stalk (↑(Subtype.mk (p := fun (x : (↑X : Type w)) ↦ x ∈ unop U) x hx) : (↑X : Type w))) : Type w))
      (β :=
      (↑(F.presheaf.stalk (↑(Subtype.mk (p := fun (x : (↑X : Type w)) ↦ x ∈ unop U) x hx) : (↑X : Type w))) : Type w))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
              CommRingCat.carrier) (Y := F.presheaf.stalk x) (F.presheaf.germ (unop U) x hx) :
            (a : (↑(F.presheaf.obj (op (unop U))) : Type w)) → (↑(F.presheaf.stalk x) : Type w))
          t :
        (↑(F.presheaf.stalk x) : Type w))
      ((CommRingCat.Hom.hom
              (F.presheaf.germ (unop U) (↑(Subtype.mk (p := fun (x : (↑X : Type w)) ↦ x ∈ unop U) x hx) : (↑X : Type w))
                ⋯) :
            (a : (↑(F.presheaf.obj U) : Type w)) → (↑(F.presheaf.stalk (↑⟨x, hx⟩ : (↑X : Type w))) : Type w))
          s :
        (↑(F.presheaf.stalk (↑(Subtype.mk (p := fun (x : (↑X : Type w)) ↦ x ∈ unop U) x hx) : (↑X : Type w))) :
          Type w)) =
    0
have inst : Eq (α :=
  (↑(F.presheaf.stalk (↑(Subtype.mk (p := fun (x : (↑X : Type w)) ↦ x ∈ unop U) x hx) : (↑X : Type w))) : Type w))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
          CommRingCat.carrier) (Y := F.presheaf.stalk x) (F.presheaf.germ (unop U) x hx) :
        (a : (↑(F.presheaf.obj (op (unop U))) : Type w)) → (↑(F.presheaf.stalk (↑⟨x, hx⟩ : (↑X : Type w))) : Type w))
      (t * s) :
    (↑(F.presheaf.stalk (↑(Subtype.mk (p := fun (x : (↑X : Type w)) ↦ x ∈ unop U) x hx) : (↑X : Type w))) : Type w))
  (0 : (↑(F.presheaf.stalk (↑(Subtype.mk (p := fun (x : (↑X : Type w)) ↦ x ∈ unop U) x hx) : (↑X : Type w))) : Type w))
Tactic: rw [← map_mul, e, map_zero]