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

Goal state before:
pp: R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (∀ (a : R), ↑v * a * ↑v⁻¹ = ↑u * a * ↑u⁻¹) ↔ ∃ α, ↑u = α • ↑v

Tactic:
← val_inv_toUnits_apply,

Goal state after:
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (∀ (a : R), ↑v * a * ↑(toUnits v)⁻¹ = ↑u * a * ↑(toUnits u)⁻¹) ↔ ∃ α, ↑u = α • ↑v
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ (∀ (a : R), ↑v * a * ↑v⁻¹ = ↑u * a * ↑u⁻¹) ↔ ∃ α, u = α • v

Tactic:
← val_inv_toUnits_apply,

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ (∀ (a : R), ↑v * a * ↑(toUnits v)⁻¹ = ↑u * a * ↑(toUnits u)⁻¹) ↔ ∃ α, u = α • v
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
a : α
b : β
c : α₂
⊢ ∀ (b_1 : α₂) (m₁ m₂ : β),
    single (f a * b_1) (b * f a • (m₁ + m₂)) = single (f a * b_1) (b * f a • m₁) + single (f a * b_1) (b * f a • m₂)

Tactic:
simp [smul_add, mul_add, single_add]

Goal state after:
Module: Mathlib.Algebra.Tropical.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddBelow s
this : Set.range untrop = Set.univ
⊢ sInf (untrop '' s) = sInf ∅

Tactic:
apply csInf_of_not_bddBelow

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddBelow s
this : Set.range untrop = Set.univ
⊢ ¬BddBelow (untrop '' s)
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
⊢ Hom.stalkMap (α ≫ β) x = Hom.stalkMap β ((ConcreteCategory.hom α.base) x) ≫ Hom.stalkMap α x

Tactic:
by
  dsimp [Hom.stalkMap, stalkFunctor, stalkPushforward]
  -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
  apply colimit.hom_ext
  rintro ⟨U, hU⟩
  simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
α β : X.Hom Y
w : α.base = β.base
h : α.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = β.c
⊢ α = β

Tactic:
rcases α with ⟨base, c⟩
  rcases β with ⟨base', c'⟩
  dsimp at w
  subst w
  dsimp at h
  erw [whiskerRight_id', comp_id] at h
  subst h
  rfl

Goal state after:
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
⊢ eqToHom ⋯ = (eqToHom ⋯).app (op U✝)

pp: 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✝))

Tactic:
eqToHom_app

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ eqToHom ⋯ = eqToHom ⋯

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.Spec

Goal state before:
pp: R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (locallyRingedSpaceMap (f ≫ g)).toHom = (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f).toHom

Tactic:
rw [Spec.locallyRingedSpaceMap_toHom, Spec.sheafedSpaceMap_comp]

Goal state after:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom = (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f).toHom
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Mono f

Tactic:
← H.isoRestrict_hom_ofRestrict

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Mono ((isoRestrict f).hom ≫ Y.ofRestrict ⋯)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ app (inv f) U = X.presheaf.map (eqToHom ⋯).op ≫ inv (app f (inv f ⁻¹ᵁ U))

Tactic:
rw [IsIso.eq_comp_inv, ← comp_app, congr_app (IsIso.hom_inv_id f), id_app, Category.id_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
s t : Set ↑Γ(X, U)
h : s ⊆ t
⊢ X.zeroLocus t ⊆ X.zeroLocus s

Tactic:
simp only [Set.subset_def, Scheme.mem_zeroLocus_iff]
  exact fun x H f hf hxf ↦ H f (h hf) hxf

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
ι : Sort u_1
κ : ι → Sort u_2
s : (i : ι) → κ i → X.Opens
⊢ f ''ᵁ ⨆ i, ⨆ j, s i j = ⨆ i, ⨆ j, f ''ᵁ s i j

Tactic:
by
  ext : 1
  simp [Set.image_iUnion₂]

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

Goal state before:
pp: X✝ Y Z : Scheme
𝒰✝ : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
X : Scheme
𝒰 : X.OpenCover
H : CompactSpace ↥X
this : ∃ t, ⋃ x ∈ t, Set.range ⇑(𝒰.f (Cover.idx 𝒰 x)) = ⊤
t : Finset ↥X := this.choose
x : ↥X
h' : ∃ i, x ∈ ⋃ (_ : i ∈ Classical.choose this), Set.range ⇑(𝒰.f (Cover.idx 𝒰 i))
⊢ ∃ y, x ∈ Set.range ⇑(𝒰.f (Cover.idx 𝒰 ↑y))

Tactic:
rcases h' with ⟨y, _, ⟨hy, rfl⟩, hy'⟩

Goal state after:
X✝ Y Z : Scheme
𝒰✝ : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
X : Scheme
𝒰 : X.OpenCover
H : CompactSpace ↥X
this : ∃ t, ⋃ x ∈ t, Set.range ⇑(𝒰.f (Cover.idx 𝒰 x)) = ⊤
t : Finset ↥X := this.choose
x y : ↥X
hy : y ∈ Classical.choose this
hy' : x ∈ (fun h ↦ Set.range ⇑(𝒰.f (Cover.idx 𝒰 y))) hy
⊢ ∃ y, x ∈ Set.range ⇑(𝒰.f (Cover.idx 𝒰 ↑y))
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀
⊢ (pullbackCoverAffineRefinementObjIso f 𝒰 i).inv ≫
      (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).f i =
    (Precoverage.ZeroHypercover.pullback₁ (Cover.pullbackHom 𝒰 f i.fst) (𝒰.X i.fst).affineCover).f i.snd ≫
      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i.fst

Tactic:
simp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
    PreZeroHypercover.pullback₁_X, AffineOpenCover.openCover_X, AffineOpenCover.openCover_f,
    pullbackCoverAffineRefinementObjIso, Iso.trans_inv, asIso_inv, Iso.symm_inv, Category.assoc,
    PreZeroHypercover.pullback₁_f, pullbackSymmetry_inv_comp_fst, IsIso.inv_comp_eq,
    limit.lift_π_assoc, PullbackCone.mk_pt, cospan_left, PullbackCone.mk_π_app,
    pullbackSymmetry_hom_comp_fst]
  convert!
    pullbackSymmetry_inv_comp_snd_assoc ((𝒰.X i.1).affineCover.f i.2) (pullback.fst _ _) _ using 2
  exact pullbackRightPullbackFstIso_hom_snd _ _ _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑X.toTopCat
⊢ op U = (Opens.map f.base).op.obj (op ((opensFunctor f).obj U))

Tactic:
have := Set.preimage_image_eq U.1 H.base_open.injective
        dsimp at this
        simp [Opens.map_def, this]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ pullback.fst (f ≫ g) (Scheme.Opens.ι U) ≫ f =
    (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι ≫ (g ⁻¹ᵁ U).ι

Tactic:
←
    pullback.condition,

Goal state after:
case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ pullback.fst (f ≫ g) (Scheme.Opens.ι U) ≫ f =
    (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.fst f (g ⁻¹ᵁ U).ι ≫ f
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e'_3
X : Scheme
inst✝ : IsAffine X
e_2✝ : X.instTopologicalSpaceCarrierCarrier = (Scheme.forgetToTop.obj X).str
V : Opens ↥X
⊢ V ∈ Set.range X.basicOpen ↔
    V ∈
      {x |
        ∃ U ∈ Set.range PrimeSpectrum.basicOpen,
          { carrier := ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' ↑U, is_open' := ⋯ } = x}

Tactic:
simp only [Set.mem_range, exists_exists_eq_and, Set.mem_ofPred,
    ← Opens.coe_inj (V := V), ← Scheme.toSpecΓ_preimage_basicOpen]

Goal state after:
case e'_3
X : Scheme
inst✝ : IsAffine X
e_2✝ : X.instTopologicalSpaceCarrierCarrier = (Scheme.forgetToTop.obj X).str
V : Opens ↥X
⊢ (∃ y, ↑(X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen y) = ↑V) ↔
    ∃ a,
      ↑{ carrier := ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' ↑(PrimeSpectrum.basicOpen a),
            is_open' := ⋯ } =
        ↑V
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
r : ↑R
⊢ let U := basicOpen r;
  (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
        (forgetToSheafedSpace.map (X.toΓSpec ≫ Spec.locallyRingedSpaceMap f)).hom.c.app (op U)) ≫
      (forgetToSheafedSpace.obj X).presheaf.map (eqToHom ⋯) =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U)

Tactic:
U

Goal state after:
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
        (forgetToSheafedSpace.map (X.toΓSpec ≫ Spec.locallyRingedSpaceMap f)).hom.c.app (op U)) ≫
      (forgetToSheafedSpace.obj X).presheaf.map (eqToHom ⋯) =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
g : S →+* P
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
W : Opens ↑(PrimeSpectrum.Top P)
hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U
hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op W))
⊢ ↑((comap (g.comp f) U W ⋯) s) p = ↑(((comap g V W hVW).comp (comap f U V hUV)) s) p

Tactic:
rw [comap_apply, Localization.localRingHom_comp _ (PrimeSpectrum.comap g p.1).asIdeal]

Goal state after:
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
g : S →+* P
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
W : Opens ↑(PrimeSpectrum.Top P)
hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U
hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op W))
⊢ ((Localization.localRingHom (PrimeSpectrum.comap g ↑p).asIdeal (↑p).asIdeal g ?hJK).comp
        (Localization.localRingHom (PrimeSpectrum.comap (g.comp f) ↑p).asIdeal (PrimeSpectrum.comap g ↑p).asIdeal f
          ?hIJ))
      (↑s ⟨PrimeSpectrum.comap (g.comp f) ↑p, ⋯⟩) =
    ↑(((comap g V W hVW).comp (comap f U V hUV)) s) p

case hIJ
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
g : S →+* P
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
W : Opens ↑(PrimeSpectrum.Top P)
hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U
hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op W))
⊢ (PrimeSpectrum.comap (g.comp f) ↑p).asIdeal = Ideal.comap f (PrimeSpectrum.comap g ↑p).asIdeal

case hJK
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
g : S →+* P
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
W : Opens ↑(PrimeSpectrum.Top P)
hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U
hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op W))
⊢ (PrimeSpectrum.comap g ↑p).asIdeal = Ideal.comap g (↑p).asIdeal
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
U✝ : X.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X, U✝)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
⊢ Arrow.mk (Scheme.Hom.stalkMap f x) ≅
    Arrow.mk
      (CommRingCat.ofHom
        (Localization.localRingHom (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal (hV.primeIdealOf ⟨x, hx⟩).asIdeal
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯))

Tactic:
let := Y.presheaf.algebra_section_stalk ⟨f x, hVU hx⟩
  have := hU.isLocalization_stalk ⟨f x, hVU hx⟩
  let := X.presheaf.algebra_section_stalk ⟨x, hx⟩
  have := hV.isLocalization_stalk ⟨x, hx⟩
  refine Arrow.isoMk' _ _ ?_ ?_ ?_
  · exact ((IsLocalization.algEquiv (hU.primeIdealOf ⟨f x, hVU hx⟩).asIdeal.primeCompl
      (Y.presheaf.stalk (f x))
      (Localization.AtPrime (hU.primeIdealOf ⟨f x, hVU hx⟩).asIdeal)).toCommRingCatIso:)
  · exact ((IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl
      (X.presheaf.stalk x)
      (Localization.AtPrime (hV.primeIdealOf ⟨x, hx⟩).asIdeal)).toCommRingCatIso:)
  · rw [← Iso.comp_inv_eq]
    ext1
    apply IsLocalization.ringHom_ext
      (hU.primeIdealOf ⟨f x, hVU hx⟩).asIdeal.primeCompl
    ext a
    dsimp [← AlgEquiv.symm_toRingEquiv]
    simp only [IsLocalization.map_eq, RingHom.id_apply, Localization.localRingHom_to_map,
      RingHomCompTriple.comp_apply]
    simp only [RingHom.algebraMap_toAlgebra, Scheme.Hom.germ_stalkMap_apply, Scheme.Hom.appLE,
      homOfLE_leOfHom, CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply,
      X.presheaf.germ_res_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
x : ↥(Spec Γ(X, U))
this : (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ ↑x.asIdeal
⊢ x ∈ ⇑hU.fromSpec ⁻¹' X.zeroLocus s ↔ x ∈ PrimeSpectrum.zeroLocus s

Tactic:
simpa [← hU.fromSpec_image_basicOpen, -not_not] using! this

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
U : Set ↑(D.U i)
x : ↑(D.V (j, i))
| x ∈ ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U

Tactic:
← Set.preimage_image_eq U (D.ι_injective _)

Goal state after:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
x : ↑(D.V (j, i))
| x ∈
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹'
      ⇑(ConcreteCategory.hom (D.ι i)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ (D.ι i) x = (D.ι j) y ↔
    (ConcreteCategory.hom
          (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
            D.isoCarrier.inv))
        x =
      (ConcreteCategory.hom D.isoCarrier.inv)
        ((ConcreteCategory.hom
            (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι j))
          y)

Tactic:
simp_rw [← D.ι_isoCarrier_inv]

Goal state after:
D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ (ConcreteCategory.hom
          (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              i ≫
            D.isoCarrier.inv))
        x =
      (ConcreteCategory.hom
          (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              j ≫
            D.isoCarrier.inv))
        y ↔
    (ConcreteCategory.hom
          (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              i ≫
            D.isoCarrier.inv))
        x =
      (ConcreteCategory.hom D.isoCarrier.inv)
        ((ConcreteCategory.hom
            (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              j))
          y)
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
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 (fV 𝒰 f g i j) (fV 𝒰 f g i k)

pp: case 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.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)

Tactic:
· apply pullback.hom_ext
    · apply pullback.hom_ext
      · simp_rw [Category.assoc, cocycle_fst_fst_fst 𝒰 f g i j k]
      · simp_rw [Category.assoc, cocycle_fst_fst_snd 𝒰 f g i j k]
    · simp_rw [Category.assoc, cocycle_fst_snd 𝒰 f g i j k]

Goal state after:
case 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.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case f
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 : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀) →
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).X x ⟶ (gluing 𝒰 f g).glued

pp: case hf
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 y : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀),
    pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f y) ≫
        ?f x =
      pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f y) ≫
        ?f y

Tactic:
· exact fun i ↦ (pullbackSymmetry _ _).hom ≫
      pullback.map _ _ _ _ (𝟙 _) s.snd f (Category.id_comp _).symm s.condition ≫ (gluing 𝒰 f g).ι i

Goal state after:
case hf
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 y : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀),
    pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f y) ≫
        (pullbackSymmetry s.fst (𝒰.f x)).hom ≫
          pullback.map (𝒰.f x) s.fst (𝒰.f x ≫ f) g (𝟙 (𝒰.X x)) s.snd f ⋯ ⋯ ≫ (gluing 𝒰 f g).ι x =
      pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f y) ≫
        (pullbackSymmetry s.fst (𝒰.f y)).hom ≫
          pullback.map (𝒰.f y) s.fst (𝒰.f y ≫ f) g (𝟙 (𝒰.X y)) s.snd f ⋯ ⋯ ≫ (gluing 𝒰 f g).ι 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
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) ≫
      p1 𝒰 f g =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.fst

Tactic:
simp [p1, pullback.condition]

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
i : 𝒰.I₀
⊢ (pullbackP1Iso 𝒰 f g i).hom ≫ pullback.fst (𝒰.f i ≫ f) g = pullback.snd (p1 𝒰 f g) (𝒰.f i)

Tactic:
pullbackP1Iso,

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
      pullback.fst (𝒰.f i ≫ f) g =
    pullback.snd (p1 𝒰 f g) (𝒰.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
i : 𝒰.I₀
⊢ (pullbackP1Iso 𝒰 f g i).hom ≫ pullback.snd (𝒰.f i ≫ f) g = pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g

Tactic:
pullbackP1Iso,

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ 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.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g
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
i : 𝒰.I₀
⊢ (pullbackP1Iso 𝒰 f g i).inv ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i) = (gluing 𝒰 f g).ι i

Tactic:
pullbackP1Iso,

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i) =
    (gluing 𝒰 f g).ι 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
i : 𝒰.I₀
⊢ (pullbackP1Iso 𝒰 f g i).inv ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i) = pullback.fst (𝒰.f i ≫ f) g

Tactic:
pullbackP1Iso,

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i) =
    pullback.fst (𝒰.f i ≫ f) g
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
x✝ : ↥Y
⊢ x✝ ∈ ↑(iSup Subtype.val) ↔ x✝ ∈ ↑⊤

Tactic:
simp [← hU]

Goal state after: