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

Goal state before:
pp: case mul_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 c✝ * Star.star a✝¹) (Star.star (b✝ * c✝))

Tactic:
star_mul

Goal state after:
case mul_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 c✝ * Star.star a✝¹) (Star.star c✝ * Star.star b✝)
Module: Mathlib.Algebra.Star.RingQuot

Goal state before:
pp: case mul_right
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 b✝ c✝
h : Rel r (Star.star b✝) (Star.star c✝)
⊢ Rel r (Star.star b✝ * Star.star a✝¹) (Star.star (a✝¹ * c✝))

Tactic:
star_mul

Goal state after:
case mul_right
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 b✝ c✝
h : Rel r (Star.star b✝) (Star.star c✝)
⊢ Rel r (Star.star b✝ * Star.star a✝¹) (Star.star c✝ * Star.star a✝¹)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
⊢ (single x r * f).coeff y = r * x • f.coeff z

Tactic:
have : (f.sum fun a b ↦ ite (x * a = y) (0 * x • b) 0) = 0 := by simp

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : (f.sum fun a b ↦ if x * a = y then 0 * x • b else 0) = 0
⊢ (single x r * f).coeff y = r * x • f.coeff z
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toRingedSpace.toPresheafedSpace
hx : x ∈ U
⊢ ¬IsUnit 0

Tactic:
isUnit_zero_iff

Goal state after:
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toRingedSpace.toPresheafedSpace
hx : x ∈ U
⊢ ¬0 = 1
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : x ∈ V
hf : IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)
⊢ ∃ t ⊆ {x | ∃ (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)}, IsOpen t ∧ x ∈ t

Tactic:
use V.1

Goal state after:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : x ∈ V
hf : IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)
⊢ V.carrier ⊆ {x | ∃ (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)} ∧
    IsOpen V.carrier ∧ x ∈ V.carrier
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ X.toRestrictTop ≫ X.ofRestrict ⋯ = 𝟙 X

Tactic:
by
    ext
    · rfl
    · erw [comp_c, ofRestrict_top_c, toRestrictTop_c, eqToHom_map, whiskerRight_id', comp_id,
        eqToHom_trans, eqToHom_refl]
      rfl

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_3
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i ↦ ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).obj U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))),
    (fun s ↦ IsGluing (X.sheafToTypes T).obj U sf' s) y → y = gl
⊢ ∀ (y : ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (iSup U)))),
    (fun s ↦ (subpresheafToTypes P.toPrelocalPredicate).IsGluing U sf s) y → y = ⟨gl, ⋯⟩

Tactic:
intro gl' hgl'
      refine Subtype.ext ?_
      exact gl_uniq gl'.1 fun i ↦ congr_arg Subtype.val (hgl' i)

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1.refine_2
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : (ConcreteCategory.hom ((P.cocone x).ι.app U)) ⟨fU, hU⟩ = (ConcreteCategory.hom ((P.cocone x).ι.app V)) ⟨fV, hV⟩
W : OpenNhds x
iU : W ⟶ unop U
iV : W ⟶ unop V
w : ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
⊢ (ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            U))
        ⟨fU, hU⟩ =
      (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop (op W))) x ⋯)) ⟨fun w ↦ fU (iU w), ⋯⟩ ∧
    (ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            V))
        ⟨fV, hV⟩ =
      (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop (op W))) x ⋯)) ⟨fun w ↦ fU (iU w), ⋯⟩

Tactic:
· exact ⟨colimit_sound iU.op (Subtype.ext rfl), colimit_sound iV.op (Subtype.ext (funext w).symm)⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op U' ⟶ op U
⊢ Y.presheaf.map i ≫ appLE f U V e = appLE f U' V ⋯

Tactic:
by
  rw [Hom.appLE, f.naturality_assoc, ← Functor.map_comp]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P✝ P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.IsStableUnderBaseChange
ι : Type (u + 1)
S : Scheme
X : ι → Scheme
f : (i : ι) → X i ⟶ S
hf : (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑(f i)) ∧ ∀ (i : ι), P (f i)
Y : Scheme
g : Y ⟶ S
T : ι → Scheme
p₁ : (i : ι) → T i ⟶ Y
p₂ : (i : ι) → T i ⟶ X i
H : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : ↥Y
i : ι
y : ↥(X i)
hy : (f i) y = g x
this : HasPullback g (f i)
w : ↥(pullback g (f i))
hw : (pullback.fst g (f i)) w = x
⊢ ∃ i, x ∈ Set.range ⇑(p₁ i)

Tactic:
use i, (H i).isoPullback.inv w

Goal state after:
case h
P✝ P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.IsStableUnderBaseChange
ι : Type (u + 1)
S : Scheme
X : ι → Scheme
f : (i : ι) → X i ⟶ S
hf : (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑(f i)) ∧ ∀ (i : ι), P (f i)
Y : Scheme
g : Y ⟶ S
T : ι → Scheme
p₁ : (i : ι) → T i ⟶ Y
p₂ : (i : ι) → T i ⟶ X i
H : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : ↥Y
i : ι
y : ↥(X i)
hy : (f i) y = g x
this : HasPullback g (f i)
w : ↥(pullback g (f i))
hw : (pullback.fst g (f i)) w = x
⊢ (p₁ i) (⋯.isoPullback.inv w) = x
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
inst✝ : JointlySurjective K
X : Scheme
𝒰 : Cover K X
⊢ ⋃ i, Set.range ⇑(𝒰.f i) = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]
  intro x
  rw [Set.mem_iUnion]
  exact 𝒰.exists_eq x

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: case refine_1
K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
x : ↥X
⊢ ∃ i, x ∈ Set.range ⇑({ I₀ := J, X := obj, f := map }.f i)

pp: case refine_2
K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
⊢ ∀ (i : { I₀ := J, X := obj, f := map }.I₀), P ({ I₀ := J, X := obj, f := map }.f i)

Tactic:
· obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq x
      obtain ⟨i, rfl⟩ := e₁.surjective i
      use i, (e₂ i).inv y
      simp [h]

Goal state after:
case refine_2
K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
⊢ ∀ (i : { I₀ := J, X := obj, f := map }.I₀), P ({ I₀ := J, X := obj, f := map }.f i)
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
x : ↥X
h :
  (ConcreteCategory.hom (Hom.app (𝒰.f (Cover.idx 𝒰 x)) U)) f =
    (ConcreteCategory.hom (Hom.app (𝒰.f (Cover.idx 𝒰 x)) U)) g
⊢ (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) f = (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) g

Tactic:
rw [← IsOpenImmersion.map_ΓIso_inv] at h

Goal state after:
case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
x : ↥X
h :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op ≫ (IsOpenImmersion.ΓIso (𝒰.f (Cover.idx 𝒰 x)) U).inv)) f =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op ≫ (IsOpenImmersion.ΓIso (𝒰.f (Cover.idx 𝒰 x)) U).inv)) g
⊢ (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) f = (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) g
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsLimit
    (PullbackCone.mk
      (forgetToSheafedSpace.map
        { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ })
      (forgetToSheafedSpace.map (Y.ofRestrict ⋯)) ⋯)

Tactic:
apply isLimitOfIsLimitPullbackConeMap SheafedSpace.forgetToPresheafedSpace

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsLimit
    (PullbackCone.mk
      (SheafedSpace.forgetToPresheafedSpace.map
        (forgetToSheafedSpace.map
          { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ }))
      (SheafedSpace.forgetToPresheafedSpace.map (forgetToSheafedSpace.map (Y.ofRestrict ⋯))) ⋯)
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: case mpr.refine_1
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
e₁ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
⊢ W ≤ U ⊓ W ⊔ V ⊓ W

Tactic:
rw [← inf_sup_right]

Goal state after:
case mpr.refine_1
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
e₁ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
⊢ W ≤ (U ⊔ V) ⊓ W
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x ∈ basicOpen 1

Tactic:
by rw [basicOpen_one]; trivial

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case h₀
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := ⋯
rhs : pullback s v ⟶ pullback t v := ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ lhs) ≫
      pullback.fst t v =
    (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ rhs) ≫
      pullback.fst t v

Tactic:
simp [lhs, rhs, equalizer.condition f g]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := ⋯
rhs : pullback s v ⟶ pullback t v := ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ lhs) ≫
      pullback.snd t v =
    (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ rhs) ≫
      pullback.snd t v

Tactic:
simp [lhs, rhs, equalizer.condition f g]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Opens ↥Y
hU : IsAffineOpen U
x : ↥X
hx : f x ∈ U
h :
  ∀ (g : ↑(Y.presheaf.obj (op U))),
    (ConcreteCategory.hom (Scheme.Hom.stalkMap f x)) ((ConcreteCategory.hom (Y.presheaf.germ U (f x) hx)) g) = 0 →
      (ConcreteCategory.hom (Y.presheaf.germ U (f x) hx)) g = 0
this : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨f x, hx⟩) := Y.presheaf.algebra_section_stalk ⟨f x, hx⟩
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
apply (hU.isLocalization_stalk ⟨f x, hx⟩).injective_of_map_algebraMap_zero

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Opens ↥Y
hU : IsAffineOpen U
x : ↥X
hx : f x ∈ U
h :
  ∀ (g : ↑(Y.presheaf.obj (op U))),
    (ConcreteCategory.hom (Scheme.Hom.stalkMap f x)) ((ConcreteCategory.hom (Y.presheaf.germ U (f x) hx)) g) = 0 →
      (ConcreteCategory.hom (Y.presheaf.germ U (f x) hx)) g = 0
this : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨f x, hx⟩) := ⋯
⊢ ∀ (x_1 : ↑Γ(Y, U)),
    (ConcreteCategory.hom (Scheme.Hom.stalkMap f x)) ((algebraMap ↑Γ(Y, U) ↑(Y.presheaf.stalk ↑⟨f x, hx⟩)) x_1) = 0 →
      (algebraMap ↑Γ(Y, U) ↑(Y.presheaf.stalk ↑⟨f x, hx⟩)) x_1 = 0
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
a b : (i : D.J) × ↑(D.U i)
x : ↑(D.V (a.fst, b.fst))
e₁ : (ConcreteCategory.hom (D.f a.fst b.fst)) x = a.snd
e₂ : (ConcreteCategory.hom (D.f b.fst a.fst)) ((ConcreteCategory.hom (D.t a.fst b.fst)) x) = b.snd
⊢ (ConcreteCategory.hom (D.f a.fst b.fst))
      ((ConcreteCategory.hom (D.t b.fst a.fst)) ((ConcreteCategory.hom (D.t a.fst b.fst)) x)) =
    a.snd

Tactic:
rw [← e₁, D.t_inv_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_3
R S : CommRingCat
f : R ⟶ S
r : ↑R
⊢ ((Spec S).isoOfEq ⋯ ≪≫ basicOpenIsoSpecAway ((CommRingCat.Hom.hom f) r)).hom ≫
      (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).hom =
    (Arrow.mk (Spec.map f ∣_ basicOpen r)).hom ≫ (basicOpenIsoSpecAway r).hom

Tactic:
· have hcomp : CommRingCat.ofHom (algebraMap R (Localization.Away r)) ≫
        CommRingCat.ofHom (Localization.awayMap f.hom r) =
        f ≫ CommRingCat.ofHom (algebraMap S (Localization.Away (f.hom r))) := by
      ext x
      simp [Localization.awayMap, IsLocalization.Away.map]
    rw [← cancel_mono (Spec.map (CommRingCat.ofHom (algebraMap R _)))]
    simp only [Arrow.mk_hom, Category.assoc, ← Spec.map_comp]
    simp [hcomp]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
⊢ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) = ⋃ i, ↑(U i)

Tactic:
ext
  constructor
  · rintro ⟨x, rfl⟩
    obtain ⟨i, ⟨x, hx'⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x
    rw [ι_fromOpenSubsetsGlue_apply]
    exact Set.subset_iUnion _ i hx'
  · rintro ⟨_, ⟨i, rfl⟩, hx⟩
    rename_i x
    exact ⟨(ofOpenSubsets U).toGlueData.ι i ⟨x, hx⟩, ι_fromOpenSubsetsGlue_apply _ _ _⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
i : ι
x : ↥(f i)
⊢ (TopCat.sigmaCofan fun x ↦ (f x).toTopCat).inj i ≫
      (colimit.isoColimitCocone
            { cocone := TopCat.sigmaCofan fun x ↦ (f x).toTopCat,
              isColimit := TopCat.sigmaCofanIsColimit fun x ↦ (f x).toTopCat }).inv ≫
        (PreservesCoproduct.iso Scheme.forgetToTop f).symm.hom =
    Scheme.forgetToTop.map (Sigma.ι f i)

Tactic:
refine (colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.sigmaCofanIsColimit _⟩ _ _).trans ?_

Goal state after:
ι : Type u
f : ι → Scheme
i : ι
x : ↥(f i)
⊢ colimit.ι (Discrete.functor fun x ↦ (f x).toTopCat) { as := i } ≫
      (PreservesCoproduct.iso Scheme.forgetToTop f).symm.hom =
    Scheme.forgetToTop.map (Sigma.ι f i)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
⊢ (((pullbackSymmetry s.fst (𝒰.f b)).hom ≫ pullback.map (𝒰.f b) s.fst (𝒰.f b ≫ f) g (𝟙 (𝒰.X b)) s.snd f ⋯ ⋯) ≫
        (gluing 𝒰 f g).ι b) ≫
      p2 𝒰 f g =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.snd

Tactic:
simp [p2]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case hom
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
⊢ pullback (p1 𝒰 f g) (𝒰.f i) ⟶ pullback (𝒰.f i ≫ f) g

Tactic:
exact
      pullback.lift (pullback.snd _ _) (pullback.fst _ _ ≫ p2 𝒰 f g)
        (by rw [← pullback.condition_assoc, Category.assoc, p_comm])

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
⊢ (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯) ≫
      pullback.snd (𝒰.f i ≫ f) g =
    𝟙 (pullback (𝒰.f i ≫ f) g) ≫ pullback.snd (𝒰.f i ≫ f) g

Tactic:
simp [p2]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
X : Scheme
inst✝ : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
⊢ IsAffineOpen (iSup U)

Tactic:
by
  have := isOpenImmersion_sigmaDesc _ (fun i ↦ (U i).ι)
    (fun i j e ↦ by convert hU' e; simp [← Opens.coe_disjoint])
  convert! isAffineOpen_opensRange (Sigma.desc fun i ↦ (U i).ι)
  · ext
    simp [(sigmaMk _).symm.exists_congr_left, ← Scheme.Hom.comp_apply, Scheme.Opens.exists_toScheme]
  · have (i : _) : IsAffine _ := hU i
    infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift 𝒰).I₀
⊢ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫ pullback.snd f g =
    ((Iso.refl (pullback ((Cover.ulift 𝒰).f i ≫ f) g)).hom ≫
        (gluing (Cover.ulift 𝒰) f g).ι ((Equiv.refl (Cover.ulift 𝒰).I₀) i) ≫
          (limit.isoLimitCone
              { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
                isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv) ≫
      pullback.snd f g

Tactic:
simp [p2]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
X : Scheme
ι : Type v
inst✝ : Small.{u, v} ι
Y : ι → Scheme
f : (i : ι) → Y i ⟶ X
hf : ∀ (i : ι), P (f i)
⊢ P (Sigma.desc f)

Tactic:
IsZariskiLocalAtSource.iff_of_openCover (P := P) (Scheme.IsLocallyDirected.openCover _)

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
X : Scheme
ι : Type v
inst✝ : Small.{u, v} ι
Y : ι → Scheme
f : (i : ι) → Y i ⟶ X
hf : ∀ (i : ι), P (f i)
⊢ ∀ (i : (Scheme.IsLocallyDirected.openCover (Discrete.functor Y)).I₀),
    P ((Scheme.IsLocallyDirected.openCover (Discrete.functor Y)).f i ≫ Sigma.desc f)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.right
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j : (MultispanShape.prod D.J).R
⊢ (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
      limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)) =
    𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j))

Tactic:
· simp_rw [Category.assoc]
    rw [Category.id_comp]
    apply π_ιInvApp_π

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: case hP₂
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
x✝¹ : Continuous[inst✝¹, inst✝] f
x✝ : IsOpen[inst✝] s
hf : ∀ (x : α), closure[inst✝] {f x} ⊆ f '' closure[inst✝¹] {x}
x : α
hx : x ∈ f ⁻¹' s
y : β
hy : y ∈ s
hcl : ⟨y, hy⟩ ∈ closure[instTopologicalSpaceSubtype] {s.restrictPreimage f ⟨x, hx⟩}
⊢ ⟨y, hy⟩ ∈ s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {⟨x, hx⟩}

Tactic:
simp only [closure_subtype, Set.restrictPreimage_mk, Set.image_singleton] at hcl

Goal state after:
case hP₂
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
x✝¹ : Continuous[inst✝¹, inst✝] f
x✝ : IsOpen[inst✝] s
hf : ∀ (x : α), closure[inst✝] {f x} ⊆ f '' closure[inst✝¹] {x}
x : α
hx : x ∈ f ⁻¹' s
y : β
hy : y ∈ s
hcl : y ∈ closure[inst✝] {f x}
⊢ ⟨y, hy⟩ ∈ s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {⟨x, hx⟩}
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: ⊢ RespectsIso fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f

Tactic:
apply surjective_stableUnderComposition.respectsIso

Goal state after:
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), Function.Surjective ⇑e.toRingHom