awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.CommRingCat
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)

Tactic:
IsLocalization.injective (M := m) (S := Localization m) ?_

Premises used: IsLocalization.injective, Localization
-- 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 : m ≤ (↑(F.presheaf.obj U) : Type w)⁰
⊢ 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:
refine IsLocalization.injective (M := m) (S := Localization m) ?_

Premises used: IsLocalization.injective, Localization
-- 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 : m ≤ nonZeroDivisorsRight (↑(F.presheaf.obj U) : Type w)
⊢ m ≤ (↑(F.presheaf.obj U) : Type w)⁰

Tactic:
rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]

Premises used: nonZeroDivisorsRight_eq_nonZeroDivisors
-- 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
s : (↑(F.presheaf.obj U) : Type w)
hs : s ∈ m
t : (↑(F.presheaf.obj U) : Type w)
e : t * s = 0
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))
⊢ t = 0

Tactic:
apply section_ext F (unop U)

Premises used: Opposite.unop, TopCat.Presheaf.section_ext
-- 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
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
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))
⊢ 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:
rw [map_zero]

Premises used: map_zero
-- 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
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
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))
                ⋯) :
            (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
⊢ 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:
apply (Submonoid.mem_iInf.mp hs ⟨x, hx⟩).2

Premises used: Subtype.mk, And.right, Iff.mp, Submonoid.mem_iInf
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X_1 : TopCat
R_1 : TopCommRingCat
X Y : TopCatᵒᵖ
f : X ⟶ Y
R : TopCommRingCat
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀
    (x y :
      unop X ⟶
        Functor.obj
          (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u_1}) ↦
            { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
            TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CD := carrier))
          R),
    f.unop ≫ (x * y) = f.unop ≫ x * f.unop ≫ y
⊢ ∀
    (x y :
      unop X ⟶
        Functor.obj
          (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u_1}) ↦
            { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
            TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CD := carrier))
          R),
    f.unop ≫ (x * y) = f.unop ≫ x * f.unop ≫ y

Tactic:
cat_disch
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X_1 : TopCat
R_1 : TopCommRingCat
X Y : TopCatᵒᵖ
f : X ⟶ Y
R : TopCommRingCat
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀
    (x y :
      unop X ⟶
        Functor.obj
          (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u_1}) ↦
            { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
            TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CD := carrier))
          R),
    f.unop ≫ (x + y) = f.unop ≫ x + f.unop ≫ y
⊢ ∀
    (x y :
      unop X ⟶
        Functor.obj
          (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u_1}) ↦
            { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
            TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CD := carrier))
          R),
    f.unop ≫ (x + y) = f.unop ≫ x + f.unop ≫ y

Tactic:
cat_disch
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X_1 : TopCat
R_1 : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x : (↑(unop X) : Type u)
⊢ Eq (α :=
    (↑(Functor.obj
          (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
            { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
            TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
          S) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            unop X) (Y :=
            Functor.obj
              (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
                { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
                TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
              S)
            (1 ≫
              CategoryTheory.Functor.map
                (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
                  { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC :=
                  TopCommRingCat.α) TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD :=
                  carrier))
                φ) :
          (a : (↑(unop X) : Type u)) → (↑((forget₂ TopCommRingCat TopCat).obj S) : Type u))
        x :
      (↑(Functor.obj
            (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
              { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
              TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
            S) :
        Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (unop X)
            (Functor.obj
              (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
                { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
                TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
              S)
            1 :
          (a : (↑(unop X) : Type u)) → (↑((forget₂ TopCommRingCat TopCat).obj S) : Type u))
        x :
      (↑(Functor.obj
            (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
              { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
              TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
            S) :
        Type u))

Tactic:
φ.1.map_one

Premises used: RingHom.map_one, Subtype.val
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X_1 : TopCat
R_1 : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x : (↑(unop X) : Type u)
⊢ Eq (α :=
    (↑(Functor.obj
          (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
            { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
            TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
          S) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            unop X) (Y :=
            Functor.obj
              (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
                { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
                TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
              S)
            (1 ≫
              CategoryTheory.Functor.map
                (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
                  { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC :=
                  TopCommRingCat.α) TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD :=
                  carrier))
                φ) :
          (a : (↑(unop X) : Type u)) → (↑((forget₂ TopCommRingCat TopCat).obj S) : Type u))
        x :
      (↑(Functor.obj
            (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
              { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
              TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
            S) :
        Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (unop X)
            (Functor.obj
              (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
                { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
                TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
              S)
            1 :
          (a : (↑(unop X) : Type u)) → (↑((forget₂ TopCommRingCat TopCat).obj S) : Type u))
        x :
      (↑(Functor.obj
            (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
              { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
              TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
            S) :
        Type u))

Tactic:
exact φ.1.map_one

Premises used: RingHom.map_one, Subtype.val
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X_1 : TopCat
R_1 : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x : (↑(unop X) : Type u)
⊢ Eq (α :=
    (↑(Functor.obj
          (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
            { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
            TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
          S) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            unop X) (Y :=
            Functor.obj
              (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
                { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
                TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
              S)
            (0 ≫
              CategoryTheory.Functor.map
                (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
                  { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC :=
                  TopCommRingCat.α) TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD :=
                  carrier))
                φ) :
          (a : (↑(unop X) : Type u)) → (↑((forget₂ TopCommRingCat TopCat).obj S) : Type u))
        x :
      (↑(Functor.obj
            (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
              { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
              TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
            S) :
        Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (unop X)
            (Functor.obj
              (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
                { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
                TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
              S)
            0 :
          (a : (↑(unop X) : Type u)) → (↑((forget₂ TopCommRingCat TopCat).obj S) : Type u))
        x :
      (↑(Functor.obj
            (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
              { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
              TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
            S) :
        Type u))

Tactic:
φ.1.map_zero

Premises used: RingHom.map_zero, Subtype.val
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X_1 : TopCat
R_1 : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x : (↑(unop X) : Type u)
⊢ Eq (α :=
    (↑(Functor.obj
          (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
            { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
            TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
          S) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            unop X) (Y :=
            Functor.obj
              (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
                { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
                TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
              S)
            (0 ≫
              CategoryTheory.Functor.map
                (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
                  { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC :=
                  TopCommRingCat.α) TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD :=
                  carrier))
                φ) :
          (a : (↑(unop X) : Type u)) → (↑((forget₂ TopCommRingCat TopCat).obj S) : Type u))
        x :
      (↑(Functor.obj
            (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
              { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
              TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
            S) :
        Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (unop X)
            (Functor.obj
              (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
                { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
                TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
              S)
            0 :
          (a : (↑(unop X) : Type u)) → (↑((forget₂ TopCommRingCat TopCat).obj S) : Type u))
        x :
      (↑(Functor.obj
            (forget₂ TopCommRingCat (FC := fun (R S : TopCommRingCat.{u}) ↦
              { f : R.α →+* S.α // Continuous (X := R.α) (Y := S.α) (⇑f : (a : R.α) → S.α) }) (CC := TopCommRingCat.α)
              TopCat (FD := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CD := carrier))
            S) :
        Type u))

Tactic:
exact φ.1.map_zero

Premises used: RingHom.map_zero, Subtype.val
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X_1 : TopCat
R_1 : TopCommRingCat
R : TopCommRingCat
X : TopCatᵒᵖ
hf :
  ∀ (x : (↑(continuousFunctions X R) : Type u)),
    Eq (α := (↑(continuousFunctions X R) : Type u))
      ((CommRingCat.Hom.hom (continuousFunctions.pullback (𝟙 X) R) :
            (a : (↑(continuousFunctions X R) : Type u)) → (↑(continuousFunctions X R) : Type u))
          x :
        (↑(continuousFunctions X R) : Type u))
      ((CommRingCat.Hom.hom (𝟙 (continuousFunctions X R)) :
            (a : (↑(continuousFunctions X R) : Type u)) → (↑(continuousFunctions X R) : Type u))
          x :
        (↑(continuousFunctions X R) : Type u))
⊢ continuousFunctions.pullback (𝟙 X) R = 𝟙 (continuousFunctions X R)

Tactic:
ext
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X_1 : TopCat
R_1 : TopCommRingCat
R : TopCommRingCat
X : TopCatᵒᵖ
x : (↑(continuousFunctions X R) : Type u)
⊢ Eq (α := (↑(continuousFunctions X R) : Type u))
    ((CommRingCat.Hom.hom (continuousFunctions.pullback (𝟙 X) R) :
          (a : (↑(continuousFunctions X R) : Type u)) → (↑(continuousFunctions X R) : Type u))
        x :
      (↑(continuousFunctions X R) : Type u))
    ((CommRingCat.Hom.hom (𝟙 (continuousFunctions X R)) :
          (a : (↑(continuousFunctions X R) : Type u)) → (↑(continuousFunctions X R) : Type u))
        x :
      (↑(continuousFunctions X R) : Type u))

Tactic:
rfl