awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U : (Opens (↑X : Type w))ᵒᵖ
hf :
  ∀ (x : (↑(CommRingCat.of (Localization (G.obj U))) : Type w)),
    Eq (α := (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
      ((CommRingCat.Hom.hom
              (CommRingCat.ofHom
                (IsLocalization.map (T := G.obj U) (Localization (G.obj U)) (CommRingCat.Hom.hom (𝟙 (F.obj U))) ⋯)) :
            (a : (↑(CommRingCat.of (Localization (G.obj U))) : Type w)) →
              (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
          x :
        (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
      ((CommRingCat.Hom.hom (𝟙 (CommRingCat.of (Localization (G.obj U)))) :
            (a : (↑(CommRingCat.of (Localization (G.obj U))) : Type w)) →
              (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
          x :
        (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
⊢ CommRingCat.ofHom (IsLocalization.map (T := G.obj U) (Localization (G.obj U)) (CommRingCat.Hom.hom (𝟙 (F.obj U))) ⋯) =
    𝟙 (CommRingCat.of (Localization (G.obj U)))

Tactic:
ext x
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U : (Opens (↑X : Type w))ᵒᵖ
x : (↑(CommRingCat.of (Localization (G.obj U))) : Type w)
⊢ Eq (α := (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
    ((CommRingCat.Hom.hom
            (CommRingCat.ofHom
              (IsLocalization.map (T := G.obj U) (Localization (G.obj U)) (CommRingCat.Hom.hom (𝟙 (F.obj U))) ⋯)) :
          (a : (↑(CommRingCat.of (Localization (G.obj U))) : Type w)) →
            (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
        x :
      (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
    ((CommRingCat.Hom.hom (𝟙 (CommRingCat.of (Localization (G.obj U)))) :
          (a : (↑(CommRingCat.of (Localization (G.obj U))) : Type w)) →
            (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
        x :
      (↑(CommRingCat.of (Localization (G.obj U))) : Type w))

Tactic:
IsLocalization.map_id x

Premises used: le_refl, OreLocalization, Quotient, IsLocalization.map_id
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U : (Opens (↑X : Type w))ᵒᵖ
x : (↑(CommRingCat.of (Localization (G.obj U))) : Type w)
⊢ Eq (α := (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
    ((CommRingCat.Hom.hom
            (CommRingCat.ofHom
              (IsLocalization.map (T := G.obj U) (Localization (G.obj U)) (CommRingCat.Hom.hom (𝟙 (F.obj U))) ⋯)) :
          (a : (↑(CommRingCat.of (Localization (G.obj U))) : Type w)) →
            (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
        x :
      (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
    ((CommRingCat.Hom.hom (𝟙 (CommRingCat.of (Localization (G.obj U)))) :
          (a : (↑(CommRingCat.of (Localization (G.obj U))) : Type w)) →
            (↑(CommRingCat.of (Localization (G.obj U))) : Type w))
        x :
      (↑(CommRingCat.of (Localization (G.obj U))) : Type w))

Tactic:
exact IsLocalization.map_id x

Premises used: le_refl, IsLocalization.map_id
-- Module: Mathlib.Topology.Sheaves.CommRingCat
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
simp_rw :
  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)) ⋯)))
⊢ 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 (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map (i ≫ 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)) ⋯)))

Tactic:
simp_rw [F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Topology.Sheaves.CommRingCat
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
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)) ⋯)))
    (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)) ⋯))))
⊢ 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)) ⋯)))

Tactic:
ext : 1
-- Module: Mathlib.Topology.Sheaves.CommRingCat
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
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))) ⋯)
    (@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)) ⋯))
⊢ 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)) ⋯))))

Tactic:
dsimp
-- Module: Mathlib.Topology.Sheaves.CommRingCat
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
hf 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))) ⋯)
    (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))) ⋯)
⊢ 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)) ⋯))

Tactic:
rw [IsLocalization.map_comp_map]

Premises used: IsLocalization.map_comp_map
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U : (Opens (↑X : Type w))ᵒᵖ
⊢ IsLocalization (G.obj U) (↑(G.localizationPresheaf.obj U) : Type w)

Tactic:
inferInstanceAs <| IsLocalization (G.obj U) (Localization (G.obj U))

Premises used: _private.0.TopCat.Presheaf.instIsLocalizationCarrierObjOppositeOpensCarrierCommRingCatObjLocalizationPresheaf._proof_1
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
⊢ Epi G.toLocalizationPresheaf

Tactic:
@NatTrans.epi_of_epi_app _ _ _ _ _ _ G.toLocalizationPresheaf fun U => Localization.epi' (G.obj U)

Premises used: TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf, CategoryTheory.NatTrans.epi_of_epi_app, TopCat.Presheaf
-- Module: Mathlib.Topology.Sheaves.CommRingCat
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
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)) ⋯) :
                (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)) ⋯) :
            (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))
⊢ 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

Tactic:
simp only [Submonoid.mem_comap, Submonoid.mem_iInf] at hs ⊢

Premises used: Submonoid.mem_comap, Submonoid.mem_iInf
-- Module: Mathlib.Topology.Sheaves.CommRingCat
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)
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)) ⋯) :
          (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))
⊢ 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))

Tactic:
change (F.map i.unop.op ≫ F.germ V.unop x.1 x.2) s ∈ _

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Functor.map, TopCat.Presheaf.germ, CategoryTheory.CategoryStruct.comp, Subtype.val, DFunLike.coe, Opposite.unop, Subtype.property
-- Module: Mathlib.Topology.Sheaves.CommRingCat
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)
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)) ⋯) :
          (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))
⊢ 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))

Tactic:
rw [F.germ_res]

Premises used: TopCat.Presheaf.germ_res
-- Module: Mathlib.Topology.Sheaves.CommRingCat
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.germ (unop U) (↑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))

Tactic:
hs ⟨_, i.unop.le x.2⟩

Premises used: Set.Mem, Quiver.Hom.le, Quiver.Hom.unop, Subtype.mk, Subtype.property
-- Module: Mathlib.Topology.Sheaves.CommRingCat
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.germ (unop U) (↑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))

Tactic:
exact hs ⟨_, i.unop.le x.2⟩

Premises used: Quiver.Hom.le, Quiver.Hom.unop, Subtype.mk, Subtype.property
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
C : Type u
inst_1 : Category.{v, u} C
F_1 : Presheaf CommRingCat X
G : F_1.SubmonoidPresheaf
F : Sheaf CommRingCat X
inst : ∀ (X_1 : (Opens (↑X : Type w))ᵒᵖ), Mono (F.presheaf.toTotalQuotientPresheaf.app X_1)
⊢ Mono F.presheaf.toTotalQuotientPresheaf

Tactic:
apply +allowSynthFailures NatTrans.mono_of_mono_app

Premises used: CategoryTheory.NatTrans.mono_of_mono_app
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
C : Type u
inst_1 : Category.{v, u} C
F_1 : Presheaf CommRingCat X
G : F_1.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens (↑X : Type w))ᵒᵖ
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))
⊢ Mono (F.presheaf.toTotalQuotientPresheaf.app U)

Tactic:
apply ConcreteCategory.mono_of_injective

Premises used: CategoryTheory.ConcreteCategory.mono_of_injective
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
C : Type u
inst_1 : Category.{v, u} C
F_1 : Presheaf CommRingCat X
G : F_1.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens (↑X : Type w))ᵒᵖ
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)) ⋯))
                    (↑(F.presheaf.stalk (↑x : (↑X : Type w))) : Type w)⁰))))) :
      (a : (↑(F.presheaf.obj U) : Type w)) → (↑(F.presheaf.totalQuotientPresheaf.obj U) : 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))

Tactic:
dsimp [toTotalQuotientPresheaf]

Premises used: TopCat.Presheaf.toTotalQuotientPresheaf
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
C : Type u
inst_1 : 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
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)
⊢ 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))

Tactic:
change Function.Injective (algebraMap _ (Localization m))

Premises used: Algebra.algebraMap, Localization, Function.Injective, DFunLike.coe