mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_3
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
a b : B
hx✝ : a ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a}
hy✝ : b ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a}
⊢ (mkRingHom r) a = 0 → (mkRingHom r) b = 0 → (mkRingHom r) (a + b) = 0

Tactic:
ha

Goal state after:
case refine_3
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
a b : B
hx✝ : a ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a}
hy✝ : b ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a}
ha : (mkRingHom r) a = 0
⊢ (mkRingHom r) b = 0 → (mkRingHom r) (a + b) = 0
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_4
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ ∀ (a x : B), x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} → (mkRingHom r) x = 0 → (mkRingHom r) (a • x) = 0

Tactic:
intro a x _ hx
        simp [hx]

Goal state after:
Module: Mathlib.Algebra.Star.RingQuot

Goal state before:
pp: case add_left
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
h : Rel r (Star.star a✝¹) (Star.star b✝)
⊢ Rel r (Star.star (a✝¹ + c✝)) (Star.star (b✝ + c✝))

Tactic:
| add_left _ h  =>

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : NonUnitalNonAssocSemiring k
g : SkewMonoidAlgebra k G
b : k
h : G → k → N
h0 : ∀ (i : G), h i 0 = 0
⊢ (b • g).sum h = g.sum fun x1 x2 ↦ h x1 (b * x2)

Tactic:
by
  simp [sum_def, Finsupp.sum_smul_index' h0]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
| (liftNC ↑f ⇑g) (a.sum single) * (liftNC ↑f ⇑g) b

Tactic:
← sum_single b

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
| (liftNC ↑f ⇑g) (a.sum single) * (liftNC ↑f ⇑g) (b.sum single)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : CommSemiring k
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
a : G
b : k
⊢ single a b = (algebraMap k (SkewMonoidAlgebra k G)) b * (of k G) a

Tactic:
by
  simp [coe_algebraMap, comp_apply, of_apply, single_mul_single, one_mul, smul_one, mul_one]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Monoid G
inst✝⁴ : CommSemiring k
A : Type u_3
inst✝³ : Semiring A
inst✝² : Algebra k A
a : G
b : k
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G k A
⊢ single a ((algebraMap k A) b) = (algebraMap k (SkewMonoidAlgebra A G)) b * (of A G) a

Tactic:
by
  simp [coe_algebraMap, comp_apply, of_apply, single_mul_single, one_mul, smul_one, mul_one]

Goal state after:
Module: Mathlib.Algebra.Vertex.VertexOperator

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (Function.support fun y ↦ (f y) x)
n : ℤ
v : V
⊢ ((HahnModule.of R).symm ((of_coeff f hf) v)).coeff (-n - 1) = (f (-n - 1)) v

Tactic:
of_coeff_apply_coeff

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (Function.support fun y ↦ (f y) x)
n : ℤ
v : V
⊢ (f (-n - 1)) v = (f (-n - 1)) v
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ X.presheaf.map (⋯.adjunction.counit.app U✝).op = (eqToHom ⋯).app (op U✝)

Tactic:
erw [eqToHom_map, eqToHom_app]

Goal state after:
case p
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ op U✝ = op (⋯.functor.obj ((Opens.map ⊤.inclusion').obj U✝))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsIso f ↔ IsIso f.base ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
rw [isIso_iff_isOpenImmersion_and_epi_base,
    IsOpenImmersion.iff_isIso_stalkMap, and_comm, ← and_assoc]
  refine and_congr ⟨?_, ?_⟩ Iff.rfl
  · rintro ⟨h₁, h₂⟩
    convert_to!
      IsIso
        (TopCat.isoOfHomeo
          (Equiv.toHomeomorphOfContinuousOpen
            (.ofBijective _ ⟨h₂.injective, (TopCat.epi_iff_surjective _).mp h₁⟩) h₂.continuous
            h₂.isOpenMap)).hom
    infer_instance
  · intro H; exact ⟨inferInstance, (TopCat.homeoOfIso (asIso f.base)).isOpenEmbedding⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ Function.Surjective ⇑f

Tactic:
← Set.range_eq_univ

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ Set.range ⇑f = Set.univ
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : R
f : M
g : ↥(Submonoid.powers s)
⊢ basicOpen s ≤ basicOpen ↑g

Tactic:
have := PrimeSpectrum.le_basicOpen_pow s; aesop (add simp [Submonoid.mem_powers_iff])

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: R : CommRingCat
f g : ↑R
⊢ (basicOpenIsoSpecAway (f * g)).inv ≫ (Spec R).homOfLE ⋯ =
    Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv

Tactic:
← cancel_mono (Scheme.Opens.ι _)

Goal state after:
R : CommRingCat
f g : ↑R
⊢ ((basicOpenIsoSpecAway (f * g)).inv ≫ (Spec R).homOfLE ⋯) ≫ Scheme.Opens.ι (PrimeSpectrum.basicOpen f) =
    (Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv) ≫
      Scheme.Opens.ι (PrimeSpectrum.basicOpen f)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
this : ∀ (i j : ↥U), ∃ a, ((g i * g j) ^ (a + 1) * g i) • f j = ((g i * g j) ^ (a + 1) * g j) • f i
⊢ ∃ ι x a b,
    ∃ (ibU : ∀ (i : ι), basicOpen (b i) ≤ U),
      U ≤ ⨆ i, basicOpen (b i) ∧
        (∀ (i j : ι), b j • a i = b i • a j) ∧
          ∀ (i : ι),
            (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s =
              const (a i) (b i) (basicOpen (b i)) ⋯

Tactic:
choose n hn using this

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
n : ↥U → ↥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
⊢ ∃ ι x a b,
    ∃ (ibU : ∀ (i : ι), basicOpen (b i) ≤ U),
      U ≤ ⨆ i, basicOpen (b i) ∧
        (∀ (i j : ι), b j • a i = b i • a j) ∧
          ∀ (i : ι),
            (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s =
              const (a i) (b i) (basicOpen (b i)) ⋯
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := ⋯
S : CommRingCat := ⋯
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := ⋯
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.Γgerm x)) r)

Tactic:
← toStalk_stalkMap_toΓSpec,

Goal state after:
X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit
    ((ConcreteCategory.hom
        (toStalk (↑(unop (op (Γ.obj (op X))))) ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ≫
          PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x))
      r)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
i : 𝒰.I₀
⊢ Set.range ⇑(𝒰.f i ⁻¹ᵁ U).ι = Set.range ⇑(pullback.snd U.ι (𝒰.f i))

Tactic:
rw [IsOpenImmersion.range_pullbackSnd U.ι (𝒰.f i), Opens.opensRange_ι]

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
i : 𝒰.I₀
⊢ Set.range ⇑(𝒰.f i ⁻¹ᵁ U).ι = ↑(𝒰.f i ⁻¹ᵁ U)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ equalizer.ι f g ≫ prod.lift f g = (equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y)

Tactic:
ext <;> simp [equalizer.condition f g]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case w
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ PrimeSpectrum.comap (CommRingCat.Hom.hom (f.c.app (op ⊤) ≫ X.presheaf.Γgerm x))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)) =
    PrimeSpectrum.comap
      ((CommRingCat.Hom.hom (Hom.stalkMap f x)).comp
        (CommRingCat.Hom.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x))))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))

Tactic:
← CommRingCat.hom_comp

Goal state after:
case w
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ PrimeSpectrum.comap (CommRingCat.Hom.hom (f.c.app (op ⊤) ≫ X.presheaf.Γgerm x))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)) =
    PrimeSpectrum.comap (CommRingCat.Hom.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x) ≫ Hom.stalkMap f x))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ↑x ∈ X.basicOpen r
h₂ : X.basicOpen r ≤ V
⊢ X.basicOpen ((CommRingCat.Hom.hom U.topIso.hom) r) ≤ V ∧ ↑x ∈ X.basicOpen ((CommRingCat.Hom.hom U.topIso.hom) r)

Tactic:
by simp [Scheme.Opens.toScheme_presheaf_obj, h₁, h₂]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
s : Cofork f g
⊢ ⇑(hom s.π) ∘ ⇑(hom f) = ⇑(hom s.π) ∘ ⇑(hom g)

Tactic:
by ext x; exact ConcreteCategory.congr_hom s.condition x

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs : (isLocallyFraction R M).pred s
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
W : Opens ↑(PrimeSpectrum.Top R)
m : ↑⟨PrimeSpectrum.comap σ p, ⋯⟩ ∈ W
iWU : W ⟶ U
a : M
b : R
h_frac : ∀ (x : ↥W), ∃ (hs : b ∉ (↑x).asIdeal), (fun x ↦ s (iWU x)) x = LocalizedModule.mk a ⟨b, hs⟩
q : ↑(PrimeSpectrum.Top S)
hqW : q ∈ ↑{ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ }
hqV : q ∈ ↑V
⊢ ∃ (hs : σ b ∉ (↑⟨q, ⋯⟩).asIdeal),
    (fun x ↦ comapFun f U V hUV s (({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ }.infLERight V) x))
        ⟨q, ⋯⟩ =
      LocalizedModule.mk (f a) ⟨σ b, hs⟩

Tactic:
obtain ⟨hs, H⟩ := h_frac ⟨PrimeSpectrum.comap σ q, hqW⟩

Goal state after:
R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs✝ : (isLocallyFraction R M).pred s
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
W : Opens ↑(PrimeSpectrum.Top R)
m : ↑⟨PrimeSpectrum.comap σ p, ⋯⟩ ∈ W
iWU : W ⟶ U
a : M
b : R
h_frac : ∀ (x : ↥W), ∃ (hs : b ∉ (↑x).asIdeal), (fun x ↦ s (iWU x)) x = LocalizedModule.mk a ⟨b, hs⟩
q : ↑(PrimeSpectrum.Top S)
hqW : q ∈ ↑{ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ }
hqV : q ∈ ↑V
hs : b ∉ (↑⟨PrimeSpectrum.comap σ q, hqW⟩).asIdeal
H : (fun x ↦ s (iWU x)) ⟨PrimeSpectrum.comap σ q, hqW⟩ = LocalizedModule.mk a ⟨b, hs⟩
⊢ ∃ (hs : σ b ∉ (↑⟨q, ⋯⟩).asIdeal),
    (fun x ↦ comapFun f U V hUV s (({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ }.infLERight V) x))
        ⟨q, ⋯⟩ =
      LocalizedModule.mk (f a) ⟨σ b, hs⟩
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⋃ i, (PrimeSpectrum.zeroLocus {↑i})ᶜ = Set.univ ↔ Ideal.span s = ⊤

Tactic:
rw [← Set.compl_iInter, Set.compl_univ_iff, ← PrimeSpectrum.zeroLocus_iUnion, ←
      PrimeSpectrum.zeroLocus_empty_iff_eq_top, PrimeSpectrum.zeroLocus_span]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ PrimeSpectrum.zeroLocus (⋃ i, {↑i}) = ∅ ↔ PrimeSpectrum.zeroLocus s = ∅
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U)))

Tactic:
have := ι_comp_coequalizerComparison f.toShHom g.toShHom SheafedSpace.forgetToPresheafedSpace
  dsimp at this
  rw [← PreservesCoequalizer.iso_hom] at this
  rw [← this, PresheafedSpace.comp_c_app,
    ← PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π]
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10754): this instance has to be manually added
  have : IsIso (PreservesCoequalizer.iso
      SheafedSpace.forgetToPresheafedSpace f.toShHom g.toShHom).hom.c :=
    inferInstance
  apply +allowSynthFailures RingHom.isLocalHom_comp
  · apply +allowSynthFailures RingHom.isLocalHom_comp
    · apply CommRingCat.equalizer_ι_isLocalHom'
    · apply isLocalHom_of_isIso
  · apply isLocalHom_of_isIso

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
s : Set ↥X
⊢ IsClosed s ↔ ∃ I, s = X.zeroLocus ↑I

Tactic:
by
  refine ⟨fun hs ↦ ?_, ?_⟩
  · let Z : Set (Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
    have hZ : IsClosed Z := (X.isoSpec.hom.homeomorph).isClosedMap _ hs
    obtain ⟨I, (hI : Z = _)⟩ := (PrimeSpectrum.isClosed_iff_zeroLocus_ideal _).mp hZ
    use I
    simp only [← Scheme.toSpecΓ_preimage_zeroLocus, ← hI, Z]
    symm
    exact Set.preimage_image_eq _ (bijective_of_isIso X.isoSpec.hom.base).injective
  · rintro ⟨I, rfl⟩
    exact zeroLocus_isClosed X I.carrier

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : Hom.toShHom f ≫ Hom.toShHom s.π = Hom.toShHom g ≫ Hom.toShHom s.π
y : ↑↑Y.toPresheafedSpace
h : ↑(s.pt.presheaf.stalk
      ((ConcreteCategory.hom (coequalizer.desc (Hom.toShHom s.π) e).hom.base)
        ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) y))) →+*
  ↑((coequalizerCofork f g).pt.presheaf.stalk
      ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) y)) :=
  CommRingCat.Hom.hom
    (PresheafedSpace.Hom.stalkMap (coequalizer.desc (Hom.toShHom s.π) e).hom
      ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) y))
⊢ IsLocalHom
    ((CommRingCat.Hom.hom ((coequalizerCofork f g).π.stalkMap y)).comp (CommRingCat.Hom.hom (CommRingCat.ofHom h)))

Tactic:
← CommRingCat.hom_comp

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : Hom.toShHom f ≫ Hom.toShHom s.π = Hom.toShHom g ≫ Hom.toShHom s.π
y : ↑↑Y.toPresheafedSpace
h : ↑(s.pt.presheaf.stalk
      ((ConcreteCategory.hom (coequalizer.desc (Hom.toShHom s.π) e).hom.base)
        ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) y))) →+*
  ↑((coequalizerCofork f g).pt.presheaf.stalk
      ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) y)) :=
  CommRingCat.Hom.hom
    (PresheafedSpace.Hom.stalkMap (coequalizer.desc (Hom.toShHom s.π) e).hom
      ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) y))
⊢ IsLocalHom (CommRingCat.Hom.hom (CommRingCat.ofHom h ≫ (coequalizerCofork f g).π.stalkMap y))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w.h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
x : ↑↑(D.V (k, i))
⊢ (ConcreteCategory.hom ((D.t k i).base ≫ (D.t i k).base)) x = x

Tactic:
← comp_base,

Goal state after:
case w.h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
x : ↑↑(D.V (k, i))
⊢ (ConcreteCategory.hom (D.t k i ≫ D.t i k).base) x = x
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w.refine_1
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
x : ↑↑(pullback (D.f i j) (D.f i k))
⊢ (ConcreteCategory.hom ((inv (D.t' k i j)).base ≫ (D.t' k i j).base)) x = x

Tactic:
← comp_base,

Goal state after:
case w.refine_1
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
x : ↑↑(pullback (D.f i j) (D.f i k))
⊢ (ConcreteCategory.hom (inv (D.t' k i j) ≫ D.t' k i j).base) x = x
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w.refine_2
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
x : ↑↑(pullback (D.f k i) (D.f k j))
⊢ (ConcreteCategory.hom ((D.t' k i j).base ≫ (inv (D.t' k i j)).base)) x = x

Tactic:
← comp_base,

Goal state after:
case w.refine_2
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
x : ↑↑(pullback (D.f k i) (D.f k j))
⊢ (ConcreteCategory.hom (D.t' k i j ≫ inv (D.t' k i j)).base) x = x
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀.h₀.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ t' 𝒰 f g i j k ≫
      t' 𝒰 f g j k i ≫
        t' 𝒰 f g k i j ≫
          pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
            pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.fst (𝒰.f i ≫ f) g =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.fst (𝒰.f i ≫ f) g

Tactic:
cocycle_fst_fst_fst 𝒰 f g i j k

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
H : ∀ (x : ↥X), ∃ U, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g
⊢ f = g

Tactic:
choose U hxU hU using H

Goal state after:
X Y : Scheme
f g : X ⟶ Y
U : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ U x
hU : ∀ (x : ↥X), (U x).ι ≫ f = (U x).ι ≫ g
⊢ f = g
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
g : σ → Scheme
inst✝¹ : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst✝ : ∀ (i : σ), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ IsOpenImmersion (Sigma.desc fun i ↦ α (e.symm i))

Tactic:
apply isOpenImmersion_sigmaDesc_aux
    intro i j hij
    exact hα (fun h ↦ hij (e.symm.injective h))

Goal state after: