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

Goal state before:
pp: case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ ⇑(ConcreteCategory.hom (↾⇑(ConcreteCategory.hom f.base))) ⁻¹' (imageBasicOpen f g U s).carrier =
    ⇑(ConcreteCategory.hom (↾⇑(ConcreteCategory.hom g.base))) ⁻¹' (imageBasicOpen f g U s).carrier

Tactic:
suffices
      (TopologicalSpace.Opens.map f.base).obj (imageBasicOpen f g U s) =
        (TopologicalSpace.Opens.map g.base).obj (imageBasicOpen f g U s)
      by injection this
    delta imageBasicOpen
    rw [preimage_basicOpen f, preimage_basicOpen g]
    dsimp
    rw [← ConcreteCategory.comp_apply, ← PresheafedSpace.comp_c_app,
      ← CommRingCat.comp_apply, ← PresheafedSpace.comp_c_app]
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11224): change `rw` to `erw`
    erw [SheafedSpace.congr_hom_app (coequalizer.condition f.toShHom g.toShHom),
      CommRingCat.comp_apply, X.toRingedSpace.basicOpen_res]
    apply inf_eq_right.mpr
    refine (RingedSpace.basicOpen_le _ _).trans ?_
    rw [coequalizer.condition f.toShHom g.toShHom]

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 =
    (fun x ↦
        (⇑(ConcreteCategory.hom (D.f i j)) ∘ ⇑(ConcreteCategory.hom (D.t j i)))
          ((ConcreteCategory.hom (D.t i j)) x)) ⁻¹'
      U

Tactic:
change _ = (D.t i j ≫ D.t j i ≫ _) ⁻¹' _
    rw [𝖣.t_inv_assoc]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
⊢ ofHom
        {
          toFun := fun x ↦
            ⟨(⟨↑((ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩,
          continuous_toFun := ⋯ } ≫
      pullbackSnd (h.V j k).inclusion' (h.V j i).inclusion' =
    (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').inv ≫
      pullback.fst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j

Tactic:
pullbackIsoProdSubtype_inv_fst_assoc

Goal state after:
D : GlueData
h : MkCore
i j k : h.J
⊢ ofHom
        {
          toFun := fun x ↦
            ⟨(⟨↑((ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩,
          continuous_toFun := ⋯ } ≫
      pullbackSnd (h.V j k).inclusion' (h.V j i).inclusion' =
    pullbackFst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
i : J
hx : x✝ ∈ (fun i ↦ ↑(U i)) i
⊢ x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Tactic:
rename_i x

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x : ↑(of α)
i : J
hx : x ∈ (fun i ↦ ↑(U i)) i
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))
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.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)

Tactic:
by
  simp only [t', Category.assoc, pullbackSymmetry_hom_comp_fst_assoc,
    pullbackRightPullbackFstIso_inv_snd_snd, pullback.lift_snd, Category.comp_id,
    pullbackRightPullbackFstIso_hom_snd]

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

Goal state before:
pp: 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.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))))) ≫
        (D.V (k, i)).presheaf.map (eqToHom ⋯)

Tactic:
by
  have e := (D.snd_invApp_t_app' i j k U).choose_spec
  replace e := reassoc_of% e
  rw [← e]
  simp [eqToHom_map]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X : Scheme
x✝¹ x✝ : X.Over (⊤_ Scheme)
a b : X ⟶ ⊤_ Scheme
⊢ { hom := a } = { hom := b }

Tactic:
by simp [Subsingleton.elim a b]

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

Goal state before:
pp: case hprecomp
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z), targetAffineLocally P f → targetAffineLocally P (e.hom ≫ f)

Tactic:
introv H U
    rw [morphismRestrict_comp, P.cancel_left_of_respectsIso]
    exact H U

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ P f ↔ ∀ (i : 𝒰.toPreZeroHypercover.1), Q (Scheme.Cover.pullbackHom 𝒰 f i)

Tactic:
let := isLocal_affineProperty P
  rw [iff_of_iSup_eq_top (P := P)
    (fun i ↦ ⟨_, isAffineOpen_opensRange _⟩) 𝒰.iSup_opensRange]
  exact forall_congr' fun i ↦ Q.arrow_mk_iso_iff
    (morphismRestrictOpensRange f _)

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

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

Tactic:
by
  ext j
  induction j with | op j => ?_
  rcases j with (⟨j, k⟩ | ⟨j⟩)
  · rw [← limit.w (componentwiseDiagram 𝖣.diagram.multispan _)
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))),
      ← Category.assoc, Category.id_comp]
    congr 1
    simp_rw [Category.assoc]
    apply π_ιInvApp_π
  · simp_rw [Category.assoc]
    rw [Category.id_comp]
    apply π_ιInvApp_π

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
⊢ Set.range ⇑f = Set.range ⇑g

Tactic:
rw [← hge]

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
e : X ⟶ Y
inst✝ : Surjective e
hge : e ≫ g = f
⊢ Set.range ⇑(e ≫ g) = Set.range ⇑g
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case mp
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
s' : Finset S
h₁ : ↑s' ⊆ s
h₂ : Ideal.span ↑s' = ⊤
⊢ ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)

Tactic:
exact ⟨s', h₂, fun t ht ↦ hs t (h₁ ht)⟩

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
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
⊢ ∃ ι s,
    ∃ (_ : Ideal.span (Set.range s) = ⊤),
      ∃ Sₜ x x_1,
        ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
          ∀ (i : ι), P ((algebraMap S' (Sₜ i)).comp (IsLocalization.Away.map R' S' f r))

Tactic:
let rₐ (a : s) : Localization.Away a.val := algebraMap _ _ (f r)

Goal state after:
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
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
rₐ : (a : ↑s) → Localization.Away ↑a := fun a ↦ (algebraMap S (Localization.Away ↑a)) (f r)
⊢ ∃ ι s,
    ∃ (_ : Ideal.span (Set.range s) = ⊤),
      ∃ Sₜ x x_1,
        ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
          ∀ (i : ι), P ((algebraMap S' (Sₜ i)).comp (IsLocalization.Away.map R' S' f r))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case to_basicOpen
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
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
U : ↑X.affineOpens
hU : ↑U ≤ f ⁻¹ᵁ Y.basicOpen r
this : X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r) = ↑U
⊢ P
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))))
          (↑(X.presheaf.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r)))))
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r)))

Tactic:
simp only [CommRingCat.hom_ofHom]

Goal state after:
case to_basicOpen
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
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
U : ↑X.affineOpens
hU : ↑U ≤ f ⁻¹ᵁ Y.basicOpen r
this : X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r) = ↑U
⊢ P
    (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))))
      (↑(X.presheaf.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r)))))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i ∈ s, ↑i
⊢ ∃ s, s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, ↑i

Tactic:
let g : s → X.affineOpens := fun V ↦ ⟨V.1 ⊓ X.basicOpen f, by
    rw [← X.basicOpen_res _ (homOfLE ((le_iSup₂ V.1 V.2).trans_eq e.symm)).op]
    exact V.1.2.basicOpen _⟩

Goal state after:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i ∈ s, ↑i
g : ↑s → ↑X.affineOpens := fun V ↦ ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
⊢ ∃ s, s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, ↑i
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
this : p.IsPrime
q : Ideal R
hq : q ∈ I.minimalPrimes
e : q ≤ p
⊢ ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height

Tactic:
have := hq.isPrime

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
this✝ : p.IsPrime
q : Ideal R
hq : q ∈ I.minimalPrimes
e : q ≤ p
this : q.IsPrime
⊢ ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ↑I.height ≤ ringKrullDim R

Tactic:
rw [Ideal.height_eq_primeHeight, Ideal.primeHeight]
  exact Order.height_le_krullDim _

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
I_top : I = ⊤
⊢ ∃ i', ⨆ (_ : I ≠ ⊤), I.height ≤ ⨆ (_ : i'.IsPrime), i'.height

Tactic:
exact ⟨⊥, by simp [I_top]⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s : ToType (X.presheaf.obj (op U))
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) (s ^ n) = (CommRingCat.Hom.hom (X.presheaf.germ U x hxU)) 0
V : Opens ↥X
hxV : x ∈ V
iU iV : V ⟶ U
e' : (ConcreteCategory.hom (X.presheaf.map iU.op)) s = 0
⊢ (ConcreteCategory.hom (X.presheaf.map iU.op ≫ X.presheaf.germ V x hxV)) s = 0

Tactic:
CommRingCat.comp_apply,

Goal state after:
X : Scheme
inst✝ : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s : ToType (X.presheaf.obj (op U))
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) (s ^ n) = (CommRingCat.Hom.hom (X.presheaf.germ U x hxU)) 0
V : Opens ↥X
hxV : x ∈ V
iU iV : V ⟶ U
e' : (ConcreteCategory.hom (X.presheaf.map iU.op)) s = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ V x hxV)) ((ConcreteCategory.hom (X.presheaf.map iU.op)) s) = 0
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
h : I.ideal = J.ideal
⊢ I = J

Tactic:
by
  obtain ⟨i, _, s, hs⟩ := I
  obtain ⟨j, _, t, ht⟩ := J
  subst h
  congr
  rw [hs, ht]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
H✝ :
  (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯))
      ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) =
    0
this : IsReduced X
H :
  (ConcreteCategory.hom (inv (Scheme.Hom.stalkMap f x)))
      ((ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
        ((ConcreteCategory.hom
            (Y.presheaf.germ { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ } (f x) ⋯))
          s)) =
    (ConcreteCategory.hom (inv (Scheme.Hom.stalkMap f x))) 0
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) (f x) ⋯)) s = 0

Tactic:
rw [← CommRingCat.comp_apply, CategoryTheory.IsIso.hom_inv_id, map_zero] at H

Goal state after:
case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
H✝ :
  (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯))
      ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) =
    0
this : IsReduced X
H :
  (ConcreteCategory.hom (𝟙 (Y.presheaf.stalk (f x))))
      ((ConcreteCategory.hom (Y.presheaf.germ { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ } (f x) ⋯))
        s) =
    0
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) (f x) ⋯)) s = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
e : Y ≅ ↑(Scheme.Hom.opensRange i) := IsOpenImmersion.isoOfRangeEq i (Scheme.Hom.opensRange i).ι ⋯
⊢ P (f ≫ i)

Tactic:
rw [show f ≫ i = f ≫ e.hom ≫ i.opensRange.ι by simp [e], ← Category.assoc]

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
e : Y ≅ ↑(Scheme.Hom.opensRange i) := IsOpenImmersion.isoOfRangeEq i (Scheme.Hom.opensRange i).ι ⋯
⊢ P ((f ≫ e.hom) ≫ (Scheme.Hom.opensRange i).ι)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case map_units
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ (y : ↥(Submonoid.powers f)), IsUnit ((algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑y)

Tactic:
rintro ⟨_, n, rfl⟩

Goal state after:
case map_units
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
n : ℕ
⊢ IsUnit ((algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑⟨(fun x ↦ f ^ x) n, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case h
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
hf✝ : ∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
x : ↥X
U : ↑Y.affineOpens
V : ↑X.affineOpens
hxV : x ∈ ↑V
e : ↑V ≤ f ⁻¹ᵁ ↑U
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ↑U ≫ X.presheaf.map (homOfLE e).op))
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Q)
    (CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.resLE f (↑U) (↑V) e)))

Tactic:
have : (toMorphismProperty (Locally Q)).RespectsIso := toMorphismProperty_respectsIso_iff.mp <|
      (isLocal_ringHomProperty P).respectsIso

Goal state after:
case h
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this✝ : P.Respects IsOpenImmersion
hf✝ : ∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
x : ↥X
U : ↑Y.affineOpens
V : ↑X.affineOpens
hxV : x ∈ ↑V
e : ↑V ≤ f ⁻¹ᵁ ↑U
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ↑U ≫ X.presheaf.map (homOfLE e).op))
this :
  (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Q)
    (CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.resLE f (↑U) (↑V) e)))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ I.support = ⊥ ↔ I = ⊤

Tactic:
refine ⟨fun H ↦ top_le_iff.mp fun U ↦ ?_, by simp +contextual⟩
  have := (U.2.fromSpec_image_zeroLocus _).trans_subset
    ((zeroLocus_inter_subset_supportSet I U).trans H.le)
  simp only [Set.subset_empty_iff, Set.image_eq_empty, Closeds.coe_bot] at this
  simp [PrimeSpectrum.zeroLocus_empty_iff_eq_top.mp this]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ I.glueDataObjMap h ≫ I.glueDataObjι V = I.glueDataObjι U ≫ X.homOfLE h

Tactic:
glueDataObjMap,

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Spec.map (CommRingCat.ofHom (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯)) ≫
      I.glueDataObjι V =
    I.glueDataObjι U ≫ X.homOfLE h
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (ConcreteCategory.hom (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f ↑x)))))
      ((ConcreteCategory.hom (Y.residue ((ConcreteCategory.hom f.base) ↑x)))
        ((ConcreteCategory.hom (Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯)) a)) =
    (ConcreteCategory.hom (X.residue ↑x))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a))

Tactic:
IsLocalRing.ResidueField.map_residue

Goal state after:
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))
      ((CommRingCat.Hom.hom (Hom.stalkMap f ↑x))
        ((ConcreteCategory.hom (Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯)) a)) =
    (ConcreteCategory.hom (X.residue ↑x))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a))
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R) ∈ U
this✝ : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R) = x
this : x ∈ U
⊢ X.presheaf.germ U x this ≫
      (ΓSpecIso (X.presheaf.stalk x)).inv ≫
        Hom.appLE (Spec.map f) ⊤ ((Opens.map (Spec.map f).base).obj ⊤) ⋯ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f

Tactic:
← (Spec.map f).app_eq_appLE,

Goal state after:
X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R) ∈ U
this✝ : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R) = x
this : x ∈ U
⊢ X.presheaf.germ U x this ≫ (ΓSpecIso (X.presheaf.stalk x)).inv ≫ Hom.app (Spec.map f) ⊤ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑U ∩ ↑↑V ∩ ↑(X.basicOpen ↑i))

Tactic:
Set.inter_inter_distrib_right

Goal state after:
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑U ∩ ↑(X.basicOpen ↑i) ∩ (↑↑V ∩ ↑(X.basicOpen ↑i)))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ I.glueDataT i i = 𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2)

Tactic:
by
    apply pullback.hom_ext
    · rw [← cancel_mono (glueDataObjι _ _)]
      simp [pullback.condition]
    · simp

Goal state after: