mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
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) ≫
        (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

Tactic:
intro i j

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

Goal state before:
pp: case h₂
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Spec.map
      ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
        (opProdIsoCoprod R S).inv.unop ≫ coprod.inr.unop) =
    Spec.map (CommRingCat.ofHom (RingHom.snd ↑R ↑S))

Tactic:
opProdIsoCoprod_inv_inr,

Goal state after:
case h₂
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Spec.map ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫ prod.snd) =
    Spec.map (CommRingCat.ofHom (RingHom.snd ↑R ↑S))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case mpr
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
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : J
xi : ↥(F.obj i)
xj : ↥(F.obj j)
⊢ (∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj) → (colimit.ι F i) xi = (colimit.ι F j) xj

pp: case mp
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
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : J
xi : ↥(F.obj i)
xj : ↥(F.obj j)
⊢ (colimit.ι F i) xi = (colimit.ι F j) xj → ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj

Tactic:
· rintro ⟨k, fi, fj, x, rfl, rfl⟩; simp only [← Scheme.Hom.comp_apply, colimit.w]

Goal state after:
case mp
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
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : J
xi : ↥(F.obj i)
xj : ↥(F.obj j)
⊢ (colimit.ι F i) xi = (colimit.ι F j) xj → ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

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)
𝒰' : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine ((𝒰' i).X j)
h𝒰' : ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀), Q (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
⊢ P.diagonal f

Tactic:
apply of_openCover 𝒱

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine ((𝒰' i).X j)
h𝒰' : ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀), Q (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := ⋯
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) := ⋯
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
⊢ ∀ (i : 𝒱.toPreZeroHypercover.1), Q (Scheme.Cover.pullbackHom 𝒱 (pullback.diagonal f) i)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op U₃))
h₄₁ : U₄ ≤ U₁
h₄₂ : U₄ ≤ U₂
h₅₁ : U₅ ≤ U₁
h₅₃ : U₅ ≤ U₃
h₆₂ : U₆ ≤ U₂
h₆₃ : U₆ ≤ U₃
h₇₄ : U₇ ≤ U₄
h₇₅ : U₇ ≤ U₅
h₇₆ : U₇ ≤ U₆
e₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
e₂ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₂

Tactic:
e₁,

Goal state after:
X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op U₃))
h₄₁ : U₄ ≤ U₁
h₄₂ : U₄ ≤ U₂
h₅₁ : U₅ ≤ U₁
h₅₃ : U₅ ≤ U₃
h₆₂ : U₆ ≤ U₂
h₆₃ : U₆ ≤ U₃
h₇₄ : U₇ ≤ U₄
h₇₅ : U₇ ≤ U₅
h₇₆ : U₇ ≤ U₆
e₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
e₂ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ *
      ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₂
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
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)))
U : ↑X.affineOpens
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))

Tactic:
induction U using of_affine_open_cover S 𝒰.iSup_opensRange with
  | basicOpen U r H =>
    simp_rw [Scheme.affineBasicOpen_coe,
      ← f.appLE_map (U := ⊤) le_top (homOfLE (X.basicOpen_le r)).op]
    have := U.2.isLocalization_basicOpen r
    exact (isLocal_ringHomProperty P).StableUnderCompositionWithLocalizationAwayTarget _ r _ H
  | openCover U s hs H =>
    apply (isLocal_ringHomProperty P).ofLocalizationSpanTarget.ofIsLocalization
      (isLocal_ringHomProperty P).respectsIso _ _ hs
    rintro r
    refine ⟨_, _, _, IsAffineOpen.isLocalization_basicOpen U.2 r, ?_⟩
    rw [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, Scheme.Hom.appLE_map]
    exact H r
  | hU i =>
    specialize H i
    rw [← (isLocal_ringHomProperty P).respectsIso.cancel_right_isIso _
      ((IsOpenImmersion.isoOfRangeEq (𝒰.f i) (S i).1.ι
      Subtype.range_coe.symm).inv.app _), ← CommRingCat.hom_comp, ← Scheme.Hom.comp_appTop,
      IsOpenImmersion.isoOfRangeEq_inv_fac_assoc, Scheme.Hom.comp_appTop,
      Scheme.Opens.ι_appTop, Scheme.Hom.appTop, Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_map] at H
    exact (f.appLE_congr _ rfl (by simp) (fun f => Q f.hom)).mp H

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
inst✝ : J.IsPrime
h : I < J
⊢ I.primeHeight + 1 ≤ J.primeHeight

Tactic:
by
  simpa [Ideal.height_eq_primeHeight] using Ideal.height_add_one_le_of_lt_of_isPrime h

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

Goal state before:
pp: case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ⨆ I, ⨆ (_ : I.IsMaximal), I.height ≤ ⨆ I, ⨆ (_ : I ≠ ⊤), I.height

pp: case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ⨆ I, ⨆ (_ : I ≠ ⊤), I.height ≤ ⨆ I, ⨆ (_ : I.IsMaximal), I.height

Tactic:
· exact iSup_mono fun I => iSup_mono' fun hI => ⟨hI.isPrime.ne_top , le_rfl⟩

Goal state after:
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ⨆ I, ⨆ (_ : I ≠ ⊤), I.height ≤ ⨆ I, ⨆ (_ : I.IsMaximal), I.height
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
R : CommRingCat
H : _root_.IsReduced ↑R
⊢ IsReduced (Spec R)

Tactic:
apply +allowSynthFailures isReduced_of_isReduced_stalk

Goal state after:
X : Scheme
R : CommRingCat
H : _root_.IsReduced ↑R
⊢ ∀ (x : ↥(Spec R)), _root_.IsReduced ↑((Spec R).presheaf.stalk x)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V) = I.ideal U

Tactic:
by
  rw [U.2.ideal_ext_iff]
  intro x hxU
  obtain ⟨f, g, hfg, hxf⟩ := exists_basicOpen_le_affine_inter U.2 V.2 x ⟨hxU, h hxU⟩
  have := I.map_ideal_basicOpen_of_eq (V := X.affineBasicOpen g) f (Subtype.ext hfg.symm)
  rw [← I.map_ideal_basicOpen] at this
  apply_fun Ideal.map (X.presheaf.germ (X.basicOpen g) x (hfg ▸ hxf)).hom at this
  simp only [Ideal.map_map, ← CommRingCat.hom_comp, affineBasicOpen_coe, X.presheaf.germ_res]
    at this ⊢
  simp only [homOfLE_leOfHom, TopCat.Presheaf.germ_res', this]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
x : ↥X
U : ↑X.affineOpens
h : x ∈ ↑U
⊢ x ∈ I.support ↔ x ∈ X.zeroLocus ↑(I.ideal U)

Tactic:
simpa [-mem_zeroLocus_iff, h] using congr(x ∈ $(I.supportSet_inter U))

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

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx : (CommRingCat.Hom.hom (f.app (Y.basicOpen s))) (IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨s ^ n, ⋯⟩) = 0
⊢ (CommRingCat.Hom.hom (f.app (Y.basicOpen s))) ((algebraMap ↑Γ(Y, ↑U) ↑Γ(Y, Y.basicOpen s)) x) = 0

Tactic:
rw [← IsLocalization.mk'_spec' (M := .powers s), map_mul, hx, mul_zero]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.snd f g =
    Spec.map (Hom.residueFieldMap (pullback.snd f g) t) ≫ Y.fromSpecResidueField ((pullback.snd f g) t)

Tactic:
simp only [Category.assoc, Triplet.specTensorTo_snd]

Goal state after:
case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInr ≫ Y.fromSpecResidueField (Triplet.ofPoint t).y =
    Spec.map (Hom.residueFieldMap (pullback.snd f g) t) ≫ Y.fromSpecResidueField ((pullback.snd f g) t)
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ (∃ a ∈ Set.range ⇑f, ∃ b ∈ Set.range ⇑g, a = b) → Nonempty ↥(pullback f g)

Tactic:
rintro ⟨_, ⟨x, rfl⟩, _, ⟨y, rfl⟩, e⟩

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
y : ↥Y
e : f x = g y
⊢ Nonempty ↥(pullback f g)
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case refine_2
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
x✝ : x ∈ ⇑f ⁻¹' Set.range ⇑g
y : ↥Y
hy : g y = f x
⊢ x ∈ Set.range ⇑(pullback.fst f g)

Tactic:
obtain ⟨a, ha⟩ := Triplet.exists_preimage (Triplet.mk' x y hy.symm)
    use a, ha.left

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case mp.right
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
t : ↥(pullback f g)
⊢ (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) t ∈ ⇑(pullback.snd f' g') ⁻¹' Set.range ⇑i₂

Tactic:
· use pullback.snd f g t
      rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply]
      simp

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

Goal state before:
pp: case right
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝¹ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
x✝ : affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen r).ι ''ᵁ ⊤)))

Tactic:
rw [Scheme.Opens.ι_image_top]

Goal state after:
case right
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝¹ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
x✝ : affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)))
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case respectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (AffineTargetMorphismProperty.toProperty fun X x x_1 x_2 ↦ IsAffine X).RespectsIso

pp: case to_basicOpen
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (r : ↑Γ(Y, ⊤)), IsAffine X → IsAffine ↑(f ⁻¹ᵁ Y.basicOpen r)

pp: case of_basicOpenCover
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (s : Finset ↑Γ(Y, ⊤)),
    Ideal.span ↑s = ⊤ → (∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)) → IsAffine X

Tactic:
· apply AffineTargetMorphismProperty.respectsIso_mk
      · rintro X Y Z e _ _ H
        have : IsAffine _ := H
        exact .of_isIso e.hom
      · exact fun _ _ _ ↦ id

Goal state after:
case to_basicOpen
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (r : ↑Γ(Y, ⊤)), IsAffine X → IsAffine ↑(f ⁻¹ᵁ Y.basicOpen r)

case of_basicOpenCover
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (s : Finset ↑Γ(Y, ⊤)),
    Ideal.span ↑s = ⊤ → (∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)) → IsAffine X
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
h : ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : ↑Y.affineOpens
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U).ι ''ᵁ ⊤)))

Tactic:
rw [Scheme.Opens.ι_image_top]

Goal state after:
case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
h : ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : ↑Y.affineOpens
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f ↑U))
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := ⋯
⊢ adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support) = ⊤

Tactic:
_root_.eq_top_iff

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
⊢ ⊤ ≤ adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case mp.inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this✝¹ :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
this✝ :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
    (RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      ∀ {X Y : Scheme} (f : X ⟶ Y),
        (HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q)
            fun {R S} [CommRing R] [CommRing S] ↦ Q) →
          IsAffineHom f →
            IsAffine Y →
              (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
                affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : ↑Y.affineOpens
this : IsAffine ↑(f ⁻¹ᵁ ↑U)
⊢ IsAffineOpen ((↑U).ι ''ᵁ ⊤)

Tactic:
rw [Scheme.Opens.ι_image_top]

Goal state after:
case mp.inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this✝¹ :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
this✝ :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
    (RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      ∀ {X Y : Scheme} (f : X ⟶ Y),
        (HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q)
            fun {R S} [CommRing R] [CommRing S] ↦ Q) →
          IsAffineHom f →
            IsAffine Y →
              (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
                affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : ↑Y.affineOpens
this : IsAffine ↑(f ⁻¹ᵁ ↑U)
⊢ IsAffineOpen ↑U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

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

Tactic:
by
  apply le_antisymm
  · rw [le_map_iff_comap_le, le_map_iff_comap_le, ← comap_comp]; exact comap_map_le _ _
  · rw [le_map_iff_comap_le, comap_comp]
    exact (comap_mono _ (comap_map_le _ _)).trans (comap_map_le _ _)

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ Dense ↑(Scheme.Hom.coborderRange f)

Tactic:
exact dense_coborder

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
i : 𝒰.I₀
n : ℕ
hn :
  (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s) ^ n *
      (Scheme.Hom.app (𝒰.f i) ⊤).hom' ((ConcreteCategory.hom φ) g) =
    0
⊢ (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ n * g)) = 0

Tactic:
by rwa [map_mul, map_mul, map_pow, map_pow]

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

Goal state before:
pp: X : Scheme
⊢ X.IsSeparated ↔ IsClosedImmersion (prod.lift (𝟙 X) (𝟙 X))

Tactic:
rw [isSeparated_iff, AlgebraicGeometry.isSeparated_iff, iff_iff_eq,
    ← MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion _ (prodIsoPullback X X).hom]

Goal state after:
X : Scheme
⊢ autoParam (IsClosedImmersion (pullback.diagonal (terminal.from X)))
      IsSeparated.isClosedImmersion_diagonal._autoParam =
    IsClosedImmersion (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
this : ∀ (U : Y.Opens), IsAffineOpen U → Function.Injective ⇑(ConcreteCategory.hom (app f U))
hU : ¬IsAffineOpen U
s : ↑Γ(Y, U)
hs : (ConcreteCategory.hom (app f U)) s = 0
x : ↥Y
hx : x ∈ Opposite.unop (Opposite.op U)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : x ∈ ↑V
hVU : V ≤ U
⊢ (ConcreteCategory.hom (app f V)) ((ConcreteCategory.hom (Y.presheaf.map (homOfLE hVU).op)) s) =
    (ConcreteCategory.hom (app f V)) ((ConcreteCategory.hom (Y.presheaf.map (homOfLE hVU).op)) 0)

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
this : ∀ (U : Y.Opens), IsAffineOpen U → Function.Injective ⇑(ConcreteCategory.hom (app f U))
hU : ¬IsAffineOpen U
s : ↑Γ(Y, U)
hs : (ConcreteCategory.hom (app f U)) s = 0
x : ↥Y
hx : x ∈ Opposite.unop (Opposite.op U)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : x ∈ ↑V
hVU : V ≤ U
⊢ (ConcreteCategory.hom (Y.presheaf.map (homOfLE hVU).op ≫ app f V)) s =
    (ConcreteCategory.hom (app f V)) ((ConcreteCategory.hom (Y.presheaf.map (homOfLE hVU).op)) 0)