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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ (pullbackConeOfLeft f g).snd.c.app x ≫
      s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).snd.base).op.obj x)) ≫
        s.pt.presheaf.map (eqToHom ⋯) ≫ (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app x =
    s.snd.c.app x

Tactic:
erw [s.snd.c.naturality_assoc]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ s.snd.c.app x ≫
      ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (⋯.adjunction.counit.app (unop x)).op ≫
        s.pt.presheaf.map (eqToHom ⋯) ≫ (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app x =
    s.snd.c.app x
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, x ∈ Set.range ⇑(p₁ i)) ∧ ∀ (i : ι), P (p₁ i)

Tactic:
refine ⟨fun x ↦ ?_, fun i ↦ P.of_isPullback (H i).flip (hf.2 i)⟩

Goal state after:
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, x ∈ Set.range ⇑(p₁ i)
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)
i : 𝒰.I₀
y : ↥(𝒰.X i)
⊢ ∃ i_1, (𝒰.f i) y ∈ Set.range ⇑({ I₀ := J, X := obj, f := map }.f i_1)

Tactic:
obtain ⟨i, rfl⟩ := e₁.surjective i

Goal state after:
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)
i : J
y : ↥(𝒰.X (e₁ i))
⊢ ∃ i_1, (𝒰.f (e₁ i)) y ∈ Set.range ⇑({ I₀ := J, X := obj, f := map }.f i_1)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ MorphismProperty.isomorphisms Scheme ≤ IsOpenImmersion

Tactic:
intro _ _ f (hf : IsIso f)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
hf : IsIso f
⊢ IsOpenImmersion f
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)

Tactic:
have := h₁.symm

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
this :
  forgetToPresheafedSpace.map (colimit.ι F i) =
    colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
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
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
r : ↥(sectionsSubalgebra R U)
a : (x : ↥U) → Localizations M ↑x
ha : a ∈ (sectionsSubmodule M U).carrier
x : ↥U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V
hVU : V ⟶ U
rx rs : R
hr : ∀ (x : ↥V), ∃ (hs : rs ∉ (↑x).asIdeal), (fun x ↦ ↑r (hVU x)) x = LocalizedModule.mk rx ⟨rs, hs⟩
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R M).pred fun x ↦ (r • a) (i x)

Tactic:
obtain ⟨W, hxW, hWU, ax, as, ha⟩ := ha x

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
r : ↥(sectionsSubalgebra R U)
a : (x : ↥U) → Localizations M ↑x
ha✝ : a ∈ (sectionsSubmodule M U).carrier
x : ↥U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V
hVU : V ⟶ U
rx rs : R
hr : ∀ (x : ↥V), ∃ (hs : rs ∉ (↑x).asIdeal), (fun x ↦ ↑r (hVU x)) x = LocalizedModule.mk rx ⟨rs, hs⟩
W : Opens ↑(PrimeSpectrum.Top R)
hxW : ↑x ∈ W
hWU : W ⟶ U
ax : M
as : R
ha : ∀ (x : ↥W), ∃ (hs : as ∉ (↑x).asIdeal), (fun x ↦ a (hWU x)) x = LocalizedModule.mk ax ⟨as, hs⟩
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R M).pred fun x ↦ (r • a) (i x)
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover X), P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P.IsLocalAtSource K

Tactic:
by
  refine .mk_of_iff fun {X Y} f R hR ↦ ?_
  rw [Precoverage.mem_iff_exists_zeroHypercover] at hR
  obtain ⟨𝒰, rfl⟩ := hR
  rw [H _ 𝒰]
  refine ⟨fun h U g ↦ ?_, fun h i ↦ h ⟨i⟩⟩
  rintro ⟨i⟩
  apply h

Goal state after:
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
⊢ D.Rel b a

Tactic:
exact ⟨D.t _ _ x, e₂, by rw [← e₁, D.t_inv_apply]⟩

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
⊢ (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι j)) y → D.Rel ⟨i, x⟩ ⟨j, y⟩

Tactic:
delta GlueData.ι
    simp_rw [← Multicoequalizer.ι_sigmaπ]
    intro h
    rw [←
      show _ = Sigma.mk i x from ConcreteCategory.congr_hom (sigmaIsoSigma.{_, u} D.U).inv_hom_id _]
    rw [←
      show _ = Sigma.mk j y from ConcreteCategory.congr_hom (sigmaIsoSigma.{_, u} D.U).inv_hom_id _]
    change InvImage D.Rel (sigmaIsoSigma.{_, u} D.U).hom _ _
    rw [← (InvImage.equivalence _ _ D.rel_equiv).eqvGen_iff]
    refine Relation.EqvGen.mono ?_ _ _ (D.eqvGen_of_π_eq h :)
    rintro _ _ ⟨x⟩
    obtain ⟨⟨⟨i, j⟩, y⟩, rfl⟩ :=
      (ConcreteCategory.bijective_of_isIso (sigmaIsoSigma.{u, u} _).inv).2 x
    unfold InvImage MultispanIndex.fstSigmaMap MultispanIndex.sndSigmaMap
    rw [sigmaIsoSigma_inv_apply]
    -- `rw [← ConcreteCategory.comp_apply]` succeeds but rewrites the wrong expression
    erw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, colimit.ι_desc_assoc,
      ← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, colimit.ι_desc_assoc]
      -- previous line now `erw` after https://github.com/leanprover-community/mathlib4/pull/13170
    erw [sigmaIsoSigma_hom_ι_apply, sigmaIsoSigma_hom_ι_apply]
    exact ⟨y, ⟨rfl, rfl⟩⟩

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mpr
D : GlueData
i j : D.J
x : ↑D.glued
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i)) →
    x ∈ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j))

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case mpr
D : GlueData
i j : D.J
x✝ : ↑D.glued
x : ↑(D.V (i, j))
hx : (ConcreteCategory.hom (D.f i j ≫ D.ι i)) x = x✝
⊢ x✝ ∈ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: 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

Tactic:
obtain rfl := (heq_eq_eq x y).mp e

Goal state after:
case refine_2
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i : σ
x : ↥(g i)
e : x ≍ x
⊢ ∃ k fi fj x_1, ((Discrete.functor g).map fi) x_1 = x ∧ ((Discrete.functor g).map fj) x_1 = x
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:
by
  apply Multicoequalizer.hom_ext
  simp [p1, p2, pullback.condition]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case hf.e_a
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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ (gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) =
    (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
        (pullbackSymmetry s.fst (𝒰.f j)).hom) ≫
      pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯

Tactic:
apply pullback.hom_ext <;> simp_rw [Category.assoc]

Goal state after:
case hf.e_a.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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫
      t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.fst (𝒰.f j ≫ f) g =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f j)).hom ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.fst (𝒰.f j ≫ f) g

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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫
      t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.snd (𝒰.f j ≫ f) g =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f j)).hom ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.snd (𝒰.f j ≫ f) g
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case e_a
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ =
    (pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)

Tactic:
apply pullback.hom_ext <;> simp_rw [Category.assoc]

Goal state after:
case e_a.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      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 =
    pullbackFstιToV 𝒰 f g i j ≫
      t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.fst (𝒰.f i ≫ f) g

case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      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 =
    pullbackFstιToV 𝒰 f g i j ≫
      t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.snd (𝒰.f i ≫ f) g
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
this :
  coprodComparison Scheme.Spec (op R) (op S) ≫
      Spec.map
        ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
          (opProdIsoCoprod R S).unop.inv) =
    coprodSpec ↑R ↑S
⊢ IsIso (coprodComparison Scheme.Spec (op R) (op S))

Tactic:
rw [(IsIso.eq_comp_inv _).mpr this]

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
this :
  coprodComparison Scheme.Spec (op R) (op S) ≫
      Spec.map
        ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
          (opProdIsoCoprod R S).unop.inv) =
    coprodSpec ↑R ↑S
⊢ IsIso
    (coprodSpec ↑R ↑S ≫
      inv
        (Spec.map
          ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
            (opProdIsoCoprod R S).unop.inv)))
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)
i j : ι
e : i ≠ j
⊢ (Disjoint on fun x ↦ Set.range ⇑(U x).ι) i j

Tactic:
by convert hU' e; simp [← Opens.coe_disjoint]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: M S T : Scheme
inst✝¹ : M.Over S
f : T ⟶ S
inst✝ : GrpObj (Over.mk (M ↘ S))
⊢ GrpObj (Over.mk (pullback (M ↘ S) f ↘ T))

Tactic:
exact Over.grpObjMkPullbackSnd

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
ha : IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hxa : x ∈ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
s : ↑Γ(X, ↑V₁)
s' : ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
this✝¹ :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
this✝ : IsLocalization.Away r' ↑Γ(Y, Y.basicOpen r')
this : IsLocalization.Away s' ↑Γ(X, X.basicOpen s')
ers : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r
heq :
  Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen s') ⋯ =
    Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
        ⋯ ≫
      CommRingCat.ofHom
        (algebraMap
          ↑(X.presheaf.1 (Opposite.op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))))
          ↑(X.presheaf.1 (Opposite.op (X.basicOpen s'))))
⊢ P
    (CommRingCat.ofHom
        (IsLocalization.Away.map (↑(Y.presheaf.1 (Opposite.op (Y.basicOpen r'))))
          (↑(X.presheaf.1 (Opposite.op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')))))
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')).hom'

Tactic:
exact hPl _ _ _ _ h₂

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

Goal state before:
pp: X : Scheme
s : Set ↑X.affineOpens
hs : s.Finite
n : ↑s → ℕ
this✝ : Finite ↑s
val✝ : Fintype ↑s
hU : IsCompact (⨆ i, ↑↑i).carrier
x f : ↑Γ(X, ⨆ i, ↑↑i)
H : (x |_ X.basicOpen f) ⋯ = 0
h₁ : ∀ (i : ↑s), ↑↑i ≤ ⨆ i, ↑↑i
hn :
  ∀ (i : ↑s),
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n i *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
      0
this : ∀ (i : ↑s), (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ Finset.univ.sup n * x) = 0
i : ↑s
⊢ (ConcreteCategory.hom (X.sheaf.obj.map (Opens.leSupr (fun i ↦ ↑↑i) i).op)) (f ^ Finset.univ.sup n * x) = 0

Tactic:
apply this

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

Goal state before:
pp: case openCover
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H✝ : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : ↥s), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(X.affineBasicOpen ↑f_1) ⋯))
r : ↑↑s
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (X.basicOpen ↑r) ⋯))

Tactic:
exact H r

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
p : Ideal R
n : ℕ
inst✝¹ : p.IsPrime
inst✝ : IsNoetherianRing R
⊢ (∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n) →
    ∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n

Tactic:
· intro H q hq e
    obtain ⟨⟨x, hx⟩, hqx, hxp⟩ :=
      @exists_le_covBy_of_lt { I : Ideal R // I.IsPrime } ⟨q, hq⟩ ⟨p, ‹_›⟩ _ _ e
    exact (Ideal.height_mono hqx).trans_lt
      (H _ hx hxp.1 (fun I hI e ↦ hxp.2 (show Subtype.mk x hx < ⟨I, hI⟩ from e)))

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case hS'
X : Scheme
⊢ (⋃₀ Set.range fun x ↦ Set.range ⇑(X.affineCover.f x)) = ⊤

Tactic:
rw [Set.top_eq_univ, Set.sUnion_range, Set.eq_univ_iff_forall]
    intro x; exact ⟨_, ⟨_, rfl⟩, X.affineCover.covers x⟩

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

Goal state before:
pp: case inst
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ IsLocalization ?M ↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f)

Tactic:
exact StructureSheaf.IsLocalization.to_basicOpen _ _

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
x : ↥X
hxU : x ∈ ↑U
⊢ x ∈ ↑Z ↔ x ∈ X.zeroLocus ↑(PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)) ∩ ↑↑U

Tactic:
rw [← U.2.fromSpec_image_zeroLocus, zeroLocus_vanishingIdeal_eq_closure,
          ← U.2.fromSpec.isOpenEmbedding.isOpenMap.preimage_closure_eq_closure_preimage
            U.2.fromSpec.continuous,
          Set.image_preimage_eq_inter_range, Z.isClosed.closure_eq, IsAffineOpen.range_fromSpec]
        simp [hxU]

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

Goal state before:
pp: X : LocallyRingedSpace
U : Opens ↑X.toTopCat
x : ↥U
f : ↑(X.presheaf.obj (op U))
⊢ (ConcreteCategory.hom (X.evaluation x)) f = 0 ↔
    ¬IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U ↑x ⋯)) f)

Tactic:
← not_iff_not,

Goal state after:
X : LocallyRingedSpace
U : Opens ↑X.toTopCat
x : ↥U
f : ↑(X.presheaf.obj (op U))
⊢ ¬(ConcreteCategory.hom (X.evaluation x)) f = 0 ↔
    ¬¬IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U ↑x ⋯)) f)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (Hom.ker f).map g = Hom.ker (f ≫ g)

Tactic:
simp [← map_bot]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ IsLocallyArtinian X ↔ ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)

Tactic:
refine ⟨fun h ↦ inferInstance, fun H ↦ ?_⟩
  refine IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology.mpr ⟨?_, ?_⟩
  · exact (isLocallyNoetherian_iff_openCover 𝒰).mpr inferInstance
  · refine discreteTopology_iff_isOpen_singleton.mpr fun x ↦ ?_
    obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
    simpa using (𝒰.f i).isOpenEmbedding.isOpenMap _ (isOpen_discrete {x})

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

Goal state before:
pp: case refine_1
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
x✝¹ : IsIntegral W
x✝ : Subsingleton ↥W
this : Field ↑Γ(W, ⊤) := ⋯
⊢ IsPullback snd (fst ≫ W.isoSpec.hom) f (W.isoSpec.inv ≫ q)

Tactic:
apply h.flip.of_iso (.refl _) (.refl _) W.isoSpec (.refl _) <;> simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ NoetherianSpace ↑(⋃ i, Set.range ⇑(𝒰.f i))

Tactic:
suffices ∀ i : 𝒰.I₀, NoetherianSpace (Set.range <| (𝒰.f i)) by
    apply NoetherianSpace.iUnion

Goal state after:
X : Scheme
inst✝ : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ ∀ (i : 𝒰.I₀), NoetherianSpace ↑(Set.range ⇑(𝒰.f i))
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
⊢ Scheme.Hom.ker (pullback.snd f g) = ⊥

Tactic:
let h𝒰 := Y.isBasis_affineOpens.isOpenCover_mem_and_le
    (S.isBasis_affineOpens.isOpenCover.comap g.base.hom)

Goal state after:
X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
h𝒰 : TopologicalSpace.IsOpenCover fun V ↦ (↑V).1 :=
  TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le (Scheme.isBasis_affineOpens Y)
    (TopologicalSpace.IsOpenCover.comap (TopologicalSpace.Opens.IsBasis.isOpenCover (Scheme.isBasis_affineOpens S))
      (TopCat.Hom.hom g.base))
⊢ Scheme.Hom.ker (pullback.snd f g) = ⊥