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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : DecidableEq G
r : k
x : G
rx : IsRightRegular x
hrx : ∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0
⊢ (f * single x r).support = image (fun x_1 ↦ x_1 * x) f.support

Tactic:
refine subset_antisymm (support_mul_single_subset f _ _) fun y hy ↦ ?_

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : DecidableEq G
r : k
x : G
rx : IsRightRegular x
hrx : ∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0
y : G
hy : y ∈ image (fun x_1 ↦ x_1 * x) f.support
⊢ y ∈ (f * single x r).support
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mp.rel.mul_left
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
h : RingConGen.Rel r a✝¹ b✝
⊢ RingConGen.Rel r (a✝¹ * c✝) (b✝ * c✝)

Tactic:
| mul_left _ h =>

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
⊢ (ringQuotToIdealQuotient r) ((mkRingHom r) x) = (Ideal.Quotient.mk (Ideal.ofRel r)) x

Tactic:
simp_rw [ringQuotToIdealQuotient, lift_def, preLift_def, mkRingHom_def]

Goal state after:
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
⊢ ({
          toFun := fun f ↦
            { toFun := fun x ↦ Quot.lift ⇑↑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ },
          invFun := fun F ↦
            ⟨F.comp
                { toFun := fun x ↦ { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                  map_add' := ⋯ },
              ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⟨Ideal.Quotient.mk (Ideal.ofRel r), ⋯⟩)
      ({ toFun := fun x ↦ { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
        x) =
    (Ideal.Quotient.mk (Ideal.ofRel r)) x
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: 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 u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
F : RingQuot s →ₐ[S] B
⊢ (fun f' ↦ preLiftAlgHom S ⋯) ((fun F ↦ ⟨F.comp (mkAlgHom S s), ⋯⟩) F) = F

Tactic:
ext
      simp only [preLiftAlgHom_def, mkAlgHom_def, mkRingHom_def,
                 AlgHom.coe_comp, AlgHom.coe_mk, RingHom.coe_mk,
                 MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a✝ b : αˢʸᵐ
a : α
this : Commute (1 + 1) a
⊢ ?m.16 a

Tactic:
rw [one_add_one_eq_two] at this

Goal state after:
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a✝ b : αˢʸᵐ
a : α
this : Commute 2 a
⊢ ?m.16 a
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Multiset (Tropical R)
⊢ untrop s.sum = (map untrop s).inf

Tactic:
by
  induction s using Multiset.induction with
  | empty => simp
  | cons s x IH => simp only [sum_cons, untrop_add, map_cons, inf_cons, ← IH]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ X.basicOpen f ≤ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)

Tactic:
· have := X.basicOpen_res (inv i) (X.presheaf.map i f)
    rw [← CommRingCat.comp_apply, ← X.presheaf.map_comp, IsIso.hom_inv_id, X.presheaf.map_id,
        CommRingCat.id_apply] at this
    rw [this]
    exact inf_le_right

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
⊢ U ≤ X.basicOpen f

Tactic:
intro x hx

Goal state after:
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ x ∈ X.basicOpen f
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥↑U) → T ↑y),
    P.pred fU →
      ∀ (fV : (y : ↥↑V) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
tU tV : (subpresheafToTypes P.toPrelocalPredicate).stalk x
h : (ConcreteCategory.hom (stalkToFiber P x)) tU = (ConcreteCategory.hom (stalkToFiber P x)) tV
⊢ ∃ W s,
    ∃ (hW : P.pred s),
      tU = (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩ ∧
        tV = (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩

Tactic:
obtain ⟨U, ⟨fU, hU⟩, rfl⟩ := jointly_surjective' tU

Goal state after:
case refine_1
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥↑U) → T ↑y),
    P.pred fU →
      ∀ (fV : (y : ↥↑V) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
tV : (subpresheafToTypes P.toPrelocalPredicate).stalk x
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
h :
  (ConcreteCategory.hom (stalkToFiber P x))
      ((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 (stalkToFiber P x)) tV
⊢ ∃ W s,
    ∃ (hW : P.pred s),
      (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 W)) x ⋯)) ⟨s, hW⟩ ∧
        tV = (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
⊢ X.basicOpen (f + g) ≤ X.basicOpen f ⊔ X.basicOpen g

Tactic:
intro x hx

Goal state after:
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↥X
hx : x ∈ X.basicOpen (f + g)
⊢ x ∈ X.basicOpen f ⊔ X.basicOpen g
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↥X
hx : x ∈ X.basicOpen (f + g)
hxU : x ∈ U
⊢ x ∈ ↑(X.basicOpen f ⊔ X.basicOpen g)

Tactic:
Opens.coe_sup,

Goal state after:
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↥X
hx : x ∈ X.basicOpen (f + g)
hxU : x ∈ U
⊢ x ∈ ↑(X.basicOpen f) ∪ ↑(X.basicOpen g)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case refine_3
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ ∀ (a x_1 : ↑Γ(X, U)), x_1 ∈ Submodule.span (↑Γ(X, U)) s → x ∉ X.basicOpen x_1 → x ∉ X.basicOpen (a • x_1)

Tactic:
simp +contextual

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
U : (Opens ↑↑X)ᵒᵖ
⊢ {
      carrier :=
        ⇑(ConcreteCategory.hom (pullback.snd f.base g.base)) ''
          ↑((↑(TopCat.Hom.frameHom (pullback.fst f.base g.base))).toFunctor.obj (unop U)),
      is_open' := ⋯ } ≤
    (↑(TopCat.Hom.frameHom g.base)).toFunctor.obj
      { carrier := ⇑(ConcreteCategory.hom f.base) '' ↑(unop U), is_open' := ⋯ }

Tactic:
rintro _ ⟨x, h₁, rfl⟩

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
U : (Opens ↑↑X)ᵒᵖ
x : ↑(pullback f.base g.base)
h₁ : x ∈ ↑((↑(TopCat.Hom.frameHom (pullback.fst f.base g.base))).toFunctor.obj (unop U))
⊢ (ConcreteCategory.hom (pullback.snd f.base g.base)) x ∈
    (↑(TopCat.Hom.frameHom g.base)).toFunctor.obj
      { carrier := ⇑(ConcreteCategory.hom f.base) '' ↑(unop U), is_open' := ⋯ }
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₁
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀ x ∈ p.asIdeal.primeCompl,
    IsUnit
      ((algebraMap ↑R
          ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                  (structureSheaf ↑S).obj).stalk
              p))
        x)

Tactic:
intro x hx

Goal state after:
case h₁
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑R
hx : x ∈ p.asIdeal.primeCompl
⊢ IsUnit
    ((algebraMap ↑R
        ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).obj).stalk
            p))
      x)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀ (x : ↑S), (toPushforwardStalkAlgHom R S p) x = 0 → ∃ m, m • x = 0

Tactic:
intro x hx

Goal state after:
case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx : (toPushforwardStalkAlgHom R S p) x = 0
⊢ ∃ m, m • x = 0
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  (PreservesPullback.iso forget f g).hom ≫ pullback.snd (forget.map f) (forget.map g) = forget.map (pullback.snd f g)
⊢ IsOpenImmersion (pullback.snd f g)

Tactic:
dsimp only [Scheme.forgetToLocallyRingedSpace, inducedFunctor_map] at this

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  (PreservesPullback.iso
          { obj := Scheme.toLocallyRingedSpace, map := fun {X Y} ↦ Scheme.Hom.toLRSHom,
            map_id := Scheme.forgetToLocallyRingedSpace._proof_1,
            map_comp := @Scheme.forgetToLocallyRingedSpace._proof_2 }
          f g).hom ≫
      pullback.snd (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g) =
    Scheme.Hom.toLRSHom (pullback.snd f g)
⊢ IsOpenImmersion (pullback.snd f g)
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case hcover
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) g
⊢ U ≤ ⨆ i, Hom.opensRange (𝒰.f (Cover.idx 𝒰 i)) ⊓ U

Tactic:
intro x hx

Goal state after:
case hcover
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) g
x : ↥X
hx : x ∈ U
⊢ x ∈ ⨆ i, Hom.opensRange (𝒰.f (Cover.idx 𝒰 i)) ⊓ U
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h_nhds.refine_1
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ a ∈ ⇑(X.affineCover.f (Cover.idx X.affineCover a)) '' (PrimeSpectrum.basicOpen s).carrier

Tactic:
exact ⟨x, hxV, e⟩

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

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U : (Opens ↑X)ᵒᵖ
⊢ CommRingCat.ofHom (IsLocalization.map (Localization (G.obj U)) (CommRingCat.Hom.hom (F.map (𝟙 U))) ⋯) =
    𝟙 (CommRingCat.of (Localization (G.obj U)))

Tactic:
simp_rw [F.map_id]

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U : (Opens ↑X)ᵒᵖ
⊢ CommRingCat.ofHom (IsLocalization.map (Localization (G.obj U)) (CommRingCat.Hom.hom (𝟙 (F.obj U))) ⋯) =
    𝟙 (CommRingCat.of (Localization (G.obj U)))
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ↑(F.presheaf.obj U) := ⋯
s : ↑(F.presheaf.obj U)
hs : s ∈ m
t : ↑(F.presheaf.obj U)
e : t * s = 0
⊢ ∀ (x : ↑X) (hx : x ∈ unop U),
    (ConcreteCategory.hom (F.presheaf.germ (unop U) x hx)) t = (ConcreteCategory.hom (F.presheaf.germ (unop U) x hx)) 0

Tactic:
intro x hx

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ↑(F.presheaf.obj U) := (F.presheaf.submonoidPresheafOfStalk fun x ↦ (↑(F.presheaf.stalk x))⁰).obj U
s : ↑(F.presheaf.obj U)
hs : s ∈ m
t : ↑(F.presheaf.obj U)
e : t * s = 0
x : ↑X
hx : x ∈ unop U
⊢ (ConcreteCategory.hom (F.presheaf.germ (unop U) x hx)) t = (ConcreteCategory.hom (F.presheaf.germ (unop U) x hx)) 0
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range
      (⇑(TopCat.Hom.hom U.ι.base) ∘
        ⇑(TopCat.Hom.hom (↑U).isoSpec.inv.base) ∘ ⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base)) =
    ↑U

Tactic:
rw [Set.range_comp, Set.range_eq_univ.mpr, Set.image_univ]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range ⇑(TopCat.Hom.hom U.ι.base) = ↑U

X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Function.Surjective
    (⇑(TopCat.Hom.hom (↑U).isoSpec.inv.base) ∘ ⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ hU.isoSpec.inv ≫ U.toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op) = Spec.map (X.presheaf.map (homOfLE ⋯).op)

Tactic:
isoSpec_inv_toSpecΓ_assoc

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Spec.map (X.presheaf.map (homOfLE ⋯).op) = Spec.map (X.presheaf.map (homOfLE ⋯).op)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case e'_3
X : LocallyRingedSpace
this :
  CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)))
          ((structureSheafInType ↑(unop (op (Γ.obj (op X)))) ↑(unop (op (Γ.obj (op X))))).obj.obj (op ⊤))) ≫
      X.toΓSpecSheafedSpace.hom.c.app (op ⊤) =
    X.presheaf.map ((Opens.map X.toΓSpecBase).obj ⊤).leTop.op
e_1✝ :
  (Γ.obj (op X) ⟶ ((pushforward CommRingCat X.toΓSpec.base).obj X.presheaf).obj (op ⊤)) =
    (CommRingCat.of ↑(Γ.obj (op X)) ⟶
      ((pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base).obj X.presheaf).obj (op ⊤))
⊢ 𝟙 (Γ.obj (op X)) = X.presheaf.map ((Opens.map X.toΓSpecBase).obj ⊤).leTop.op

Tactic:
exact (X.presheaf.map_id ..).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ X.presheaf.map (homOfLE ⋯).op ≫
      (↑U).presheaf.map (eqToHom ⋯).op ≫
        (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv) ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Tactic:
simp only [Scheme.Opens.toScheme_presheaf_map, Scheme.Opens.topIso_hom,
    Category.assoc, ← X.presheaf.map_comp_assoc]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ X.presheaf.map ((homOfLE ⋯).op ≫ ((Scheme.Hom.opensFunctor U.ι).map (eqToHom ⋯).op.unop).op ≫ (eqToHom ⋯).op) ≫
      (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed {↑x}
⊢ IsClosed {x}

Tactic:
simpa [← Set.image_singleton, Set.preimage_image_eq _ Subtype.val_injective]
      using hx.preimage U.isOpenEmbedding'.continuous

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑hU.fromSpec ⁻¹' (⨆ f, X.basicOpen ↑f).carrier = ⇑hU.fromSpec ⁻¹' U.carrier ↔
    ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ

Tactic:
simp only [Opens.iSup_def, Set.preimage_iUnion]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⋃ i, ⇑hU.fromSpec ⁻¹' ↑(X.basicOpen ↑i) = ⇑hU.fromSpec ⁻¹' U.carrier ↔
    ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
← PrimeSpectrum.zeroLocus_iUnion,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ PrimeSpectrum.zeroLocus (⋃ i, {↑i}) = ∅ ↔ Ideal.span s = ⊤
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
⊢ U ≤ ⨆ i ∈ s, X.basicOpen i

Tactic:
intro x hx

Goal state after:
case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↥X
hx : x ∈ U
⊢ x ∈ ⨆ i ∈ s, X.basicOpen i
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
⊢ ↑V ≤ ⨆ f_1, X.basicOpen ↑f_1

Tactic:
intro x hx

Goal state after:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
x : ↥X
hx : x ∈ ↑V
⊢ x ∈ ⨆ f_1, X.basicOpen ↑f_1
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑X.isoSpec.hom '' X.zeroLocus s = PrimeSpectrum.zeroLocus s

Tactic:
← X.toSpecΓ_preimage_zeroLocus

Goal state after:
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑X.isoSpec.hom '' ⇑X.toSpecΓ ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus s
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ IsColimit
    (forgetToSheafedSpace.mapCocone
      (coequalizerCofork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))

Tactic:
apply (isColimitMapCoconeCoforkEquiv _ _).symm _

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ IsColimit
    (Cofork.ofπ
      (forgetToSheafedSpace.map
        (homMk
          (coequalizer.π (Hom.toShHom (F.map WalkingParallelPairHom.left))
            (Hom.toShHom (F.map WalkingParallelPairHom.right)))
          ⋯))
      ⋯)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w
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))
⊢ (Opens.map (D.t k i).base).op.obj (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) =
    op
      ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).obj
        (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U))))))

pp: case 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))
⊢ invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
      (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
        (D.V (k, i)).presheaf.map (eqToHom ?w) =
    (D.t' k i j).c.app (op U) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U)))))

Tactic:
· delta IsOpenImmersion.opensFunctor IsOpenEmbedding.functor
    dsimp only [Functor.op, Opens.map_def, IsOpenMap.functor, unop_op, Opens.coe_mk]
    congr 2
    have := (𝖣.t_fac k i j).symm
    rw [← IsIso.inv_comp_eq] at this
    replace this := (congr_arg ((PresheafedSpace.Hom.base ·)) this).symm
    replace this := congr_arg (TopCat.Hom.hom ·) this
    replace this := congr_arg (ContinuousMap.toFun ·) this
    dsimp at this
    rw [this, Set.image_comp, Set.image_comp, Set.preimage_image_eq]
    swap
    · refine Function.HasLeftInverse.injective ⟨(D.t i k).base, fun x => ?_⟩
      rw [← ConcreteCategory.comp_apply, ← comp_base, D.t_inv, id_base, ConcreteCategory.id_apply]
    refine congr_arg (_ '' ·) ?_
    refine congr_fun ?_ _
    refine Set.image_eq_preimage_of_inverse ?_ ?_
    · intro x
      rw [← ConcreteCategory.comp_apply, ← comp_base, IsIso.inv_hom_id, id_base,
        ConcreteCategory.id_apply]
    · intro x
      rw [← ConcreteCategory.comp_apply, ← comp_base, IsIso.hom_inv_id, id_base,
        ConcreteCategory.id_apply]

Goal state after:
case 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))
⊢ invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
      (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
        (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    (D.t' k i j).c.app (op U) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U)))))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : IsOpen U
⊢ ∀ x ∈ ⇑(fromGlued 𝒰) '' U, ∃ t ⊆ ⇑(fromGlued 𝒰) '' U, IsOpen t ∧ x ∈ t

Tactic:
intro x hx

Goal state after:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : IsOpen U
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
⊢ ∃ t ⊆ ⇑(fromGlued 𝒰) '' U, IsOpen t ∧ x ∈ t
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case k
X : Scheme
𝒰✝ : X.OpenCover
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf : ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y
⊢ (b : (MultispanShape.prod (ulift 𝒰).gluedCover.J).R) → (ulift 𝒰).gluedCover.diagram.right b ⟶ Y

Tactic:
exact fun i ↦ f _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_2
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
x : ↥(g i)
y : ↥(g j)
⊢ i = j ∧ x ≍ y → ∃ k fi fj x_1, ((Discrete.functor g).map fi) x_1 = x ∧ ((Discrete.functor g).map fj) x_1 = y

Tactic:
rintro ⟨rfl, e⟩

Goal state after:
case refine_2
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i : σ
x y : ↥(g i)
e : x ≍ y
⊢ ∃ k fi fj x_1, ((Discrete.functor g).map fi) x_1 = x ∧ ((Discrete.functor g).map fj) x_1 = y
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
⊢ p1 𝒰 f g ≫ f = p2 𝒰 f g ≫ g

Tactic:
apply Multicoequalizer.hom_ext
  simp [p1, p2, pullback.condition]

Goal state after: