mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this✝¹ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens ↑↑(X.restrict hf)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this✝ : IsIso (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
this :
  (g₁ ≫ X.ofRestrict hf).c.app (op (hf.functor.obj V)) =
    (g₂ ≫ X.ofRestrict hf).c.app (op (hf.functor.obj V)) ≫ Z.presheaf.map (eqToHom ⋯)
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)

Tactic:
rw [PresheafedSpace.comp_c_app, PresheafedSpace.comp_c_app,
      PresheafedSpace.ofRestrict_c_app, Category.assoc, cancel_epi] at this

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this✝¹ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens ↑↑(X.restrict hf)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this✝ : IsIso (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
this :
  g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) =
    g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯)
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case mp
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ IsUnit
    ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))

Tactic:
delta toRingedSpace

Goal state after:
case mp
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ IsUnit
    ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case mp
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s)) →
    x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s))

Tactic:
rintro ⟨hxU, hx⟩
    rw [SetLike.mem_coe, X.toRingedSpace.mem_basicOpen _ _ hxU]
    delta toRingedSpace
    rw [← stalkMap_germ_apply]
    exact (f.stalkMap _).hom.isUnit_map hx

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : f x = g y
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
⊢ ∃ a, (pullback.snd f g) a = y

Tactic:
obtain ⟨a, ha⟩ := exists_preimage_fst_triplet_of_prop hf y x h.symm

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : f x = g y
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
a : ↥(pullback g f)
ha : (pullback.fst g f) a = y
⊢ ∃ a, (pullback.snd f g) a = y
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
R : CommRingCat
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
⊢ ∃ i, s i ∉ x.asIdeal

Tactic:
by_contra! h

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
h : ∀ (i : ι), s i ∈ x.asIdeal
⊢ False
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
R : CommRingCat
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
this : ∃ i, s i ∉ x.asIdeal
⊢ ι

Tactic:
exact this.choose

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

Goal state before:
pp: X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s = 0
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) 0

Tactic:
rw [map_zero]

Goal state after:
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s = 0
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s = 0
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (isoRestrict f).hom ≫ Y.ofRestrict ⋯ = f

Tactic:
by
  apply LocallyRingedSpace.forgetToSheafedSpace.map_injective
  exact SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict f.toShHom

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
f₁ f₂ : M
g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
H : g₁ • f₂ = g₂ • f₁
x : ↥(unop (op U))
⊢ ↑(const f₁ g₁ U hu₁) x = ↑(const f₂ g₂ U hu₂) x

Tactic:
simp [LocalizedModule.mk_eq, Localizations, Submonoid.smul_def, H]

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 : R
f : M
g : ↥(Submonoid.powers s)
⊢ (toBasicOpenₗ R M s) (LocalizedModule.mk f g) = const f (↑g) (basicOpen s) ⋯

Tactic:
obtain ⟨_, n, rfl⟩ := g

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ (toBasicOpenₗ R M s) (LocalizedModule.mk f ⟨(fun x ↦ s ^ x) n, ⋯⟩) = const f (↑⟨(fun x ↦ s ^ x) n, ⋯⟩) (basicOpen s) ⋯
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) := (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

Tactic:
rw [map_zero]

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 = 0
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ s ^ n •
      (IsLocalizedModule.lift (Submonoid.powers s) (LocalizedModule.mkLinearMap (Submonoid.powers s) M)
          (toOpenₗ R M (basicOpen s)) ⋯)
        (LocalizedModule.mk f ⟨s ^ n, ⋯⟩) =
    s ^ n • const f (s ^ n) (basicOpen s) ⋯

Tactic:
← map_smul,

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ (IsLocalizedModule.lift (Submonoid.powers s) (LocalizedModule.mkLinearMap (Submonoid.powers s) M)
        (toOpenₗ R M (basicOpen s)) ⋯)
      (s ^ n • LocalizedModule.mk f ⟨s ^ n, ⋯⟩) =
    s ^ n • const f (s ^ n) (basicOpen s) ⋯
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
⊢ ∀ {U : TopologicalSpace.Opens ↥X} {x : ↥X}, x ∈ U → ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U

Tactic:
rintro U x (hU : x ∈ (U : Set X))

Goal state after:
X : Scheme
U : TopologicalSpace.Opens ↥X
x : ↥X
hU : x ∈ ↑U
⊢ ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U
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 ((Equiv.refl 𝒰.I₀) i)))

pp: case refine_2
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
⊢ ∀ (i : 𝒰.I₀),
    𝒰.f i ∣_ U =
      (IsOpenImmersion.isoOfRangeEq (𝒰.f i ⁻¹ᵁ U).ι (pullback.snd U.ι (𝒰.f ((Equiv.refl 𝒰.I₀) i))) ⋯).hom ≫
        (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).f ((Equiv.refl 𝒰.I₀) i)

Tactic:
· dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
      PreZeroHypercover.pullback₁_I₀, Equiv.refl_apply, PreZeroHypercover.pullback₁_X]
    rw [IsOpenImmersion.range_pullbackSnd U.ι (𝒰.f i), Opens.opensRange_ι]
    exact Subtype.range_val

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
⊢ ∀ (i : 𝒰.I₀),
    𝒰.f i ∣_ U =
      (IsOpenImmersion.isoOfRangeEq (𝒰.f i ⁻¹ᵁ U).ι (pullback.snd U.ι (𝒰.f ((Equiv.refl 𝒰.I₀) i))) ⋯).hom ≫
        (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).f ((Equiv.refl 𝒰.I₀) i)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ ↑s •
      (IsLocalizedModule.lift x.asIdeal.primeCompl (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
          (ModuleCat.Hom.hom (toStalkₗ' R M x)) ⋯)
        (LocalizedModule.mk f s) =
    ↑s •
      (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
        (const f (↑s) (basicOpen ↑s) ⋯)

Tactic:
← map_smul,

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ (IsLocalizedModule.lift x.asIdeal.primeCompl (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
        (ModuleCat.Hom.hom (toStalkₗ' R M x)) ⋯)
      (↑s • LocalizedModule.mk f s) =
    ↑s •
      (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
        (const f (↑s) (basicOpen ↑s) ⋯)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ (ModuleCat.Hom.hom (toStalkₗ' R M x)) f =
    ↑s •
      (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
        (const f (↑s) (basicOpen ↑s) ⋯)

Tactic:
← map_smul,

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ (ModuleCat.Hom.hom (toStalkₗ' R M x)) f =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
      (↑s • const f (↑s) (basicOpen ↑s) ⋯)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ (Scheme.ΓSpecIso Γ(X, U)).hom ≫ Scheme.Hom.app hU.fromSpec U = (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op

Tactic:
change _ = (Spec Γ(X, U)).presheaf.map (homOfLE le_top).op
  simp [IsAffineOpen.fromSpec_app_of_le]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ (Scheme.ΓSpecIso Γ(X, U)).hom ≫ Scheme.Hom.app hU.fromSpec U = (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op

Tactic:
by
  change _ = (Spec Γ(X, U)).presheaf.map (homOfLE le_top).op
  simp [IsAffineOpen.fromSpec_app_of_le]

Goal state after:
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 : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
f' : M →ₗ[R] N :=
  let __spread.0 := f;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
⊢ ∀ (x : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl),
    IsUnit ((algebraMap R (Module.End R (LocalizedModule y.asIdeal.primeCompl N))) ↑x)

Tactic:
intro x
      have := IsLocalizedModule.map_units (S := y.asIdeal.primeCompl)
        (LocalizedModule.mkLinearMap y.asIdeal.primeCompl N) ⟨σ x, x.2⟩
      rw [Module.End.isUnit_iff] at this ⊢
      convert! this using 2 with a
      exact (IsScalarTower.algebraMap_smul ..).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hy : hU.fromSpec y ∈ U
⊢ IsLocalization y.asIdeal.primeCompl ↑((Spec Γ(X, U)).presheaf.stalk y) ↔
    IsLocalization.AtPrime (↑((structureSheaf ↑Γ(X, U)).presheaf.stalk y)) y.asIdeal

Tactic:
delta IsLocalization.AtPrime StructureSheaf.stalkAlgebra

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hy : hU.fromSpec y ∈ U
⊢ IsLocalization y.asIdeal.primeCompl ↑((Spec Γ(X, U)).presheaf.stalk y) ↔
    IsLocalization y.asIdeal.primeCompl ↑((structureSheaf ↑Γ(X, U)).presheaf.stalk y)
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j : D.J
⊢ Mono (if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i j h)

Tactic:
split_ifs <;> infer_instance

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U = ⇑(ConcreteCategory.hom (D.t i j ≫ D.t j i ≫ D.f i j)) ⁻¹' U

Tactic:
rw [𝖣.t_inv_assoc]

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 j k : 𝒰.I₀
⊢ t' 𝒰 f g i j k ≫
      pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k) ≫ pullback.fst (𝒰.f j ≫ f) g =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)

Tactic:
simp only [t', Category.assoc, pullbackSymmetry_hom_comp_fst_assoc,
    pullbackRightPullbackFstIso_inv_snd_fst_assoc, pullback.lift_fst_assoc, t_fst_fst,
    pullbackRightPullbackFstIso_hom_fst_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case e'_3.e'_4
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
e_1✝ : ↥(𝒰.X (idx 𝒰 x)) = ↥((gluedCover 𝒰).U (idx 𝒰 x))
⊢ ⇑(TopCat.Hom.hom (fromGlued 𝒰).base) ⁻¹' (fun a ↦ (fromGlued 𝒰) a) '' U = U

Tactic:
exact Set.preimage_image_eq _ 𝒰.fromGlued_injective

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝² : Category.{v, w} J
F : J ⥤ Scheme
inst✝¹ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝ : (F ⋙ forget).IsLocallyDirected
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
⊢ ∃ l fi fj fk α z,
    IsOpenImmersion α ∧
      α ≫ pullback.fst (V F i j).ι (V F i k).ι = (Hom.isoOpensRange (F.map fi)).hom ≫ (F.obj i).homOfLE ⋯ ∧
        α ≫ pullback.snd (V F i j).ι (V F i k).ι = (Hom.isoOpensRange (F.map fi)).hom ≫ (F.obj i).homOfLE ⋯ ∧ α z = x

Tactic:
by
  obtain ⟨k₁, y₁, hy₁⟩ := mem_iSup.mp ((pullback.fst (C := Scheme) _ _) x).2
  obtain ⟨k₂, y₂, hy₂⟩ := mem_iSup.mp ((pullback.snd (C := Scheme) _ _) x).2
  obtain ⟨l, hli, hlk, z, rfl, rfl⟩ :=
    (F ⋙ forget).exists_map_eq_of_isLocallyDirected k₁.2.1 k₂.2.1 y₁ y₂
      (by simpa [hy₁, hy₂] using congr($(pullback.condition (f := (V F i j).ι)) x))
  let α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
    pullback.lift
      ((F.map (hli ≫ k₁.2.1)).isoOpensRange.hom ≫ Scheme.homOfLE _
        (le_iSup_of_le ⟨l, hli ≫ k₁.2.1, hli ≫ k₁.2.2⟩ le_rfl))
      ((F.map (hli ≫ k₁.2.1)).isoOpensRange.hom ≫ Scheme.homOfLE _
        (le_iSup_of_le ⟨l, hli ≫ k₁.2.1, hlk ≫ k₂.2.2⟩ le_rfl))
      (by simp)
  have : IsOpenImmersion α := by
    apply +allowSynthFailures IsOpenImmersion.of_comp
    · exact (inferInstance : IsOpenImmersion (pullback.fst (V F i j).ι (V F i k).ι))
    · simp only [limit.lift_π, PullbackCone.mk_π_app, α]
      infer_instance
  have : α z = x := by
    apply (pullback.fst (C := Scheme) _ _).isOpenEmbedding.injective
    apply (V F i j).ι.isOpenEmbedding.injective
    rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.lift_fst_assoc]
    simpa using hy₁
  exact ⟨l, hli ≫ k₁.2.1, hli ≫ k₁.2.2, hlk ≫ k₂.2.2, α, z, ‹_›, by simp [α], by simp [α], ‹_›⟩

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)
this : IsOpenImmersion (Sigma.desc fun i ↦ (U i).ι)
⊢ IsAffine (∐ fun i ↦ ↑(U i))

Tactic:
have (i : _) : IsAffine _ := hU i

Goal state after:
ι : Type u
X : Scheme
inst✝ : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this✝ : IsOpenImmersion (Sigma.desc fun i ↦ (U i).ι)
this : ∀ (i : ι), IsAffine ↑(U i)
⊢ IsAffine (∐ fun i ↦ ↑(U i))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: I : Type u_1
inst✝¹ : Category.{v_1, u_1} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝ : ∀ (i : I), IsAffine (D.obj i)
⊢ IsAffine c.pt

Tactic:
let α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
  have (i : _) : IsIso (α.app i) := IsAffine.affine
  have : IsIso α := NatIso.isIso_of_isIso_app α
  have : c.pt ≅ Spec Γ(c.pt, ⊤) := hc.conePointUniqueUpToIso ((IsLimit.postcomposeHomEquiv
    (asIso α).symm _).symm (isLimitOfPreserves (Scheme.Γ.rightOp ⋙ Scheme.Spec) hc))
  exact .of_isIso this.hom

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

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
e : X ⟶ Y
inst✝ : Surjective e
hge : e ≫ g = f
s : ↥S
⊢ s ∈ Set.range ⇑f ↔ s ∈ Set.range ⇑g

Tactic:
rw [range_eq_range_of_surjective f g e hge]

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
y : R
hy : y ∈ Ideal.span (Set.range (mulNumerator s p))
m : ℕ
hyz : mk' (Rₜ ⟨a, ha⟩) 1 1 = mk' (Rₜ ⟨a, ha⟩) y ⟨(fun x ↦ a ^ x) m, ⋯⟩
⊢ a ∈ ↑(Ideal.span (Set.range (mulNumerator s p))).radical

Tactic:
IsLocalization.eq

Goal state after:
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
y : R
hy : y ∈ Ideal.span (Set.range (mulNumerator s p))
m : ℕ
hyz : ∃ c, ↑c * (↑⟨(fun x ↦ a ^ x) m, ⋯⟩ * 1) = ↑c * (↑1 * y)
⊢ a ∈ ↑(Ideal.span (Set.range (mulNumerator s p))).radical
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x ↦ ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
n' : ℕ
e'' : f (↑r ^ (n' + n)) * x = f (↑r ^ n' * b)
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range

Tactic:
exact ⟨n' + n, _, e''.symm⟩

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
by
  introv R hf
  obtain ⟨s, hsone, hs⟩ := hf
  rw [locally_iff_exists hPl.respectsIso]
  let rₐ (a : s) : Localization.Away a.val := algebraMap _ _ (f r)
  let Sₐ (a : s) := Localization.Away (rₐ a)
  have (a : s) :
      IsLocalization.Away (((algebraMap S (Localization.Away a.val)).comp f) r) (Sₐ a) :=
    inferInstanceAs (IsLocalization.Away (rₐ a) (Sₐ a))
  have (a : s) : IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away a.val)
    (Submonoid.map f (Submonoid.powers r))) (Sₐ a) := by
    convert! (inferInstance : IsLocalization.Away (rₐ a) (Sₐ a))
    simp [rₐ, Algebra.algebraMapSubmonoid]
  have H (a : s) : Submonoid.powers (f r) ≤
      (Submonoid.powers (rₐ a)).comap (algebraMap S (Localization.Away a.val)) := by
    simp [rₐ, Submonoid.powers_le]
  let (a : s) : Algebra S' (Sₐ a) :=
    (IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away a.val)) (H a)).toAlgebra
  have (a : s) : IsScalarTower S S' (Sₐ a) :=
    IsScalarTower.of_algebraMap_eq' (IsLocalization.map_comp (H a)).symm
  refine ⟨s, fun a ↦ algebraMap S S' a.val, ?_, Sₐ,
      inferInstance, inferInstance, fun a ↦ ?_, fun a ↦ ?_⟩
  · rw [← Set.image_eq_range, ← Ideal.map_span, hsone, Ideal.map_top]
  · convert!
    IsLocalization.commutes (T := Sₐ a) (M₁ := (Submonoid.powers r).map f) (S₁ := S') (S₂ :=
      Localization.Away a.val) (M₂ := Submonoid.powers a.val)
    simp [Algebra.algebraMapSubmonoid]
  · rw [algebraMap_toAlgebra, IsLocalization.Away.map, IsLocalization.map_comp_map]
    exact hPl ((algebraMap _ (Localization.Away a.val)).comp f) r R' (Sₐ a) (hs _ a.2)

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

Goal state before:
pp: case h₂
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y],
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)

Tactic:
introv H U
    rw [Scheme.Hom.comp_appLE, CommRingCat.hom_comp, h₁.cancel_left_isIso]
    exact H U

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

Goal state before:
pp: case e'_3
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H✝ : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ 0 = (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ?refine_1.convert_1).op)) 0

Tactic:
rw [map_zero]

Goal state after: