awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
h : g (↑j : ↥U) ^ (N + 1) • g (↑i : ↥U) ^ N • f (↑i : ↥U) = (g (↑i : ↥U) * g (↑j : ↥U)) ^ N • g (↑j : ↥U) • f (↑i : ↥U)
h₁ : g (↑i : ↥U) ^ (N + 1) • g (↑j : ↥U) ^ N • f (↑j : ↥U) = (g (↑i : ↥U) * g (↑j : ↥U)) ^ N • g (↑i : ↥U) • f (↑j : ↥U)
refine_1 :
  (g (↑i : ↥U) * g (↑j : ↥U)) ^ N • g (↑j : ↥U) • f (↑i : ↥U) =
    (g (↑i : ↥U) * g (↑j : ↥U)) ^ N • g (↑i : ↥U) • f (↑j : ↥U)
⊢ g (↑j : ↥U) ^ (N + 1) • g (↑i : ↥U) ^ N • f (↑i : ↥U) = g (↑i : ↥U) ^ (N + 1) • g (↑j : ↥U) ^ N • f (↑j : ↥U)

Tactic:
convert_to (g i * g ↑j) ^ N • g j • f i = (g i * g ↑j) ^ N • g i • f j

Premises used: HMul.hMul, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
⊢ g (↑j : ↥U) ^ (N + 1) • g (↑i : ↥U) ^ N • f (↑i : ↥U) = (g (↑i : ↥U) * g (↑j : ↥U)) ^ N • g (↑j : ↥U) • f (↑i : ↥U)

Tactic:
module
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
⊢ g (↑i : ↥U) ^ (N + 1) • g (↑j : ↥U) ^ N • f (↑j : ↥U) = (g (↑i : ↥U) * g (↑j : ↥U)) ^ N • g (↑i : ↥U) • f (↑j : ↥U)

Tactic:
module
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
⊢ (i.1, j.1) ∈ t ×ˢ t

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
⊢ n (↑i : ↥U) (↑j : ↥U) + 1 ≤ N

Tactic:
have : n i j + 1 ≤ N := (t ×ˢ t).le_sup (f := fun x ↦ n x.1 x.2 + 1) (b := ⟨_, _⟩) (by simp)
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
this : n (↑i : ↥U) (↑j : ↥U) + 1 ≤ N
refine_1 :
  (g (↑i : ↥U) * g (↑j : ↥U)) ^ (N - (n (↑i : ↥U) (↑j : ↥U) + 1)) •
      (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑j : ↥U) • f (↑i : ↥U) =
    (g (↑i : ↥U) * g (↑j : ↥U)) ^ (N - (n (↑i : ↥U) (↑j : ↥U) + 1)) •
      (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑i : ↥U) • f (↑j : ↥U)
⊢ (g (↑i : ↥U) * g (↑j : ↥U)) ^ N • g (↑j : ↥U) • f (↑i : ↥U) =
    (g (↑i : ↥U) * g (↑j : ↥U)) ^ N • g (↑i : ↥U) • f (↑j : ↥U)

Tactic:
rw [← Nat.sub_add_cancel this, pow_add, mul_smul, mul_smul]

Premises used: pow_add, Nat.sub_add_cancel, SemigroupAction.mul_smul
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
this : n (↑i : ↥U) (↑j : ↥U) + 1 ≤ N
refine_1 :
  (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑j : ↥U) • f (↑i : ↥U) =
    (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑i : ↥U) • f (↑j : ↥U)
⊢ (g (↑i : ↥U) * g (↑j : ↥U)) ^ (N - (n (↑i : ↥U) (↑j : ↥U) + 1)) •
      (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑j : ↥U) • f (↑i : ↥U) =
    (g (↑i : ↥U) * g (↑j : ↥U)) ^ (N - (n (↑i : ↥U) (↑j : ↥U) + 1)) •
      (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑i : ↥U) • f (↑j : ↥U)

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
this : n (↑i : ↥U) (↑j : ↥U) + 1 ≤ N
⊢ ((g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) * g (↑j : ↥U)) • f (↑i : ↥U) =
    ((g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) * g (↑i : ↥U)) • f (↑j : ↥U)

Tactic:
(hn i j).symm

Premises used: Eq.symm, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
this : n (↑i : ↥U) (↑j : ↥U) + 1 ≤ N
h :
  (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑j : ↥U) • f (↑i : ↥U) =
    ((g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) * g (↑j : ↥U)) • f (↑i : ↥U)
h₁ :
  (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑i : ↥U) • f (↑j : ↥U) =
    ((g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) * g (↑i : ↥U)) • f (↑j : ↥U)
⊢ (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑j : ↥U) • f (↑i : ↥U) =
    (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑i : ↥U) • f (↑j : ↥U)

Tactic:
convert! (hn i j).symm using 1

Premises used: Eq.symm, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
this : n (↑i : ↥U) (↑j : ↥U) + 1 ≤ N
⊢ (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑j : ↥U) • f (↑i : ↥U) =
    ((g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) * g (↑j : ↥U)) • f (↑i : ↥U)

Tactic:
module
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
this : n (↑i : ↥U) (↑j : ↥U) + 1 ≤ N
⊢ (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑i : ↥U) • f (↑j : ↥U) =
    ((g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) * g (↑i : ↥U)) • f (↑j : ↥U)

Tactic:
module