mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝³ : CommRing R
x✝² : CommRing S
x✝¹ : CommRing T
f : R →+* S
e : S ≃+* T
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
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)
a : S
ha : a ∈ s
⊢ P ((algebraMap T (Localization.Away (e a))).comp (e.toRingHom.comp f))

Tactic:
let e' : Localization.Away a ≃+* Localization.Away (e a) :=
        IsLocalization.ringEquivOfRingEquiv _ _ e (Submonoid.map_powers e a)

Goal state after:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝³ : CommRing R
x✝² : CommRing S
x✝¹ : CommRing T
f : R →+* S
e : S ≃+* T
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
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)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (e a) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (e a)) e ⋯
⊢ P ((algebraMap T (Localization.Away (e a))).comp (e.toRingHom.comp f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
⊢ Q.diagonal f

Tactic:
HasAffineProperty.diagonal_iff (targetAffineLocally Q)

Goal state after:
Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
⊢ (targetAffineLocally Q).diagonal f
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
T : Scheme
g : T ⟶ Y
inst✝ : HasPullback g (𝒰.f i ≫ f)
⊢ P (pullback.fst g (𝒰.f i ≫ f))

Tactic:
rw [← P.cancel_left_of_respectsIso (pullbackLeftPullbackSndIso g f _).hom,
      pullbackLeftPullbackSndIso_hom_fst]

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
T : Scheme
g : T ⟶ Y
inst✝ : HasPullback g (𝒰.f i ≫ f)
⊢ P (pullback.fst (pullback.snd g f) (𝒰.f i) ≫ pullback.fst g f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
⊢ stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ≫ e)

Tactic:
by
    simp only [stalkwise, Scheme.Hom.comp_base, TopCat.coe_comp, Function.comp_apply]
    intro x
    rw [Scheme.Hom.stalkMap_comp]
    exact (RingHom.RespectsIso.cancel_left_isIso hP _ _).mpr <| hf x

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
hP : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
this :
  (pullback.fst (Scheme.Hom.appTop (AffineScheme.ofHom f).hom).op
          (Scheme.Hom.appTop (AffineScheme.ofHom g).hom).op).unop ≫
      (PreservesPullback.iso (AffineScheme.forgetToScheme.op ⋙ Scheme.Γ).rightOp (AffineScheme.ofHom f)
            (AffineScheme.ofHom g)).hom.unop =
    Scheme.Hom.appTop (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)).hom
⊢ P
    ((CommRingCat.Hom.hom
          (pushoutIsoUnopPullback (Scheme.Hom.appTop (AffineScheme.ofHom f).hom)
              (Scheme.Hom.appTop (AffineScheme.ofHom g).hom)).hom).comp
      (CommRingCat.Hom.hom
        (pushout.inl (Scheme.Hom.appTop (AffineScheme.ofHom f).hom) (Scheme.Hom.appTop (AffineScheme.ofHom g).hom))))

Tactic:
hP'.cancel_right_isIso

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
this :
  (pullback.fst (Scheme.Hom.appTop (AffineScheme.ofHom f).hom).op
          (Scheme.Hom.appTop (AffineScheme.ofHom g).hom).op).unop ≫
      (PreservesPullback.iso (AffineScheme.forgetToScheme.op ⋙ Scheme.Γ).rightOp (AffineScheme.ofHom f)
            (AffineScheme.ofHom g)).hom.unop =
    Scheme.Hom.appTop (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)).hom
⊢ P
    (CommRingCat.Hom.hom
      (pushout.inl (Scheme.Hom.appTop (AffineScheme.ofHom f).hom) (Scheme.Hom.appTop (AffineScheme.ofHom g).hom)))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ QuasiCompact f ↔ ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)

Tactic:
rw [quasiCompact_iff]

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (⇑f ⁻¹' U)) ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
p : Ideal R
right✝ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hpp : p.IsPrime
hIp : I ≤ p
h : p.primeHeight = ↑n
⊢ ∃ p, ∃ (_ : p.IsPrime) (_ : I ≤ p), p.height = ↑n

Tactic:
exact ⟨p, hpp, hIp, h ▸ p.height_eq_primeHeight⟩

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

Goal state before:
pp: case refine_1
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
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : f x ∈ U
right✝ : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑V)) Sₜ] [IsLocalization.Away t Sₜ],
            Q ((algebraMap (↑Γ(X, ↑V)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)))
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
obtain ⟨s, hs, hfs⟩ := hf ⟨U, hU⟩ ⟨V, hV⟩ e

Goal state after:
case refine_1
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
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : f x ∈ U
right✝ : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑V)) Sₜ] [IsLocalization.Away t Sₜ],
            Q ((algebraMap (↑Γ(X, ↑V)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)))
s : Finset ↑Γ(X, ↑⟨V, hV⟩)
hs : Ideal.span ↑s = ⊤
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑⟨V, hV⟩)) Sₜ] [IsLocalization.Away t Sₜ],
      Q ((algebraMap (↑Γ(X, ↑⟨V, hV⟩)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑⟨U, hU⟩) (↑⟨V, hV⟩) e)))
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: R : CommRingCat
x : ↥(Spec R)
⊢ ringKrullDim ↑((Spec R).presheaf.stalk x) = ↑(coheight x)

Tactic:
let k : Algebra ↑R ↑((Spec R).presheaf.stalk x) := StructureSheaf.stalkAlgebra (↑R) x

Goal state after:
R : CommRingCat
x : ↥(Spec R)
k : Algebra ↑R ↑((Spec R).presheaf.stalk x) := StructureSheaf.stalkAlgebra (↑R) x
⊢ ringKrullDim ↑((Spec R).presheaf.stalk x) = ↑(coheight x)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
F : Γ(X, ↑U) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x✝ : ↑Γ(X, ↑U)
hx : x✝ ∈ PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)
x : ↥(Spec Γ(X, ↑(X.affineBasicOpen f)))
hxZ : (IsAffineOpen.fromSpec ⋯) x ∈ Z
⊢ (CommRingCat.Hom.hom F) x✝ ∈ x.asIdeal

Tactic:
refine (PrimeSpectrum.mem_vanishingIdeal _ _).mp hx
          (Spec.map (X.presheaf.map (homOfLE _).op) x) ?_

Goal state after:
case a
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
F : Γ(X, ↑U) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x✝ : ↑Γ(X, ↑U)
hx : x✝ ∈ PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)
x : ↥(Spec Γ(X, ↑(X.affineBasicOpen f)))
hxZ : (IsAffineOpen.fromSpec ⋯) x ∈ Z
⊢ (Spec.map (X.presheaf.map (homOfLE ⋯).op)) x ∈ ⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ Hom.app (X.fromSpecStalk x) U =
    X.presheaf.germ U x hxU ≫
      (ΓSpecIso (X.presheaf.stalk x)).inv ≫ (Spec (X.presheaf.stalk x)).presheaf.map (homOfLE ⋯).op

Tactic:
obtain ⟨_, ⟨V : X.Opens, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open
    hxU U.2
  rw [← hV.fromSpecStalk_eq_fromSpecStalk hxV, IsAffineOpen.fromSpecStalk, Scheme.Hom.comp_app,
    hV.fromSpec_app_of_le _ hVU, ← X.presheaf.germ_res (homOfLE hVU) x hxV]
  simp [Category.assoc, ← ΓSpecIso_inv_naturality_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
inst✝ : IsLocalRing ↑R
x : ↑R
⊢ (CommRingCat.Hom.hom (stalkClosedPointIso R).inv) x =
    (CommRingCat.Hom.hom (StructureSheaf.toStalk (↑R) (closedPoint ↑R))) x

Tactic:
exact (StructureSheaf.stalkIso _ _).commutes _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk (f (closedPoint ↑R)) = f

Tactic:
by
  obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open
    (Set.mem_univ (f (closedPoint R))) isOpen_univ
  have := IsAffineOpen.SpecMap_appLE_fromSpec f hU (isAffineOpen_top _)
    (preimage_eq_top_of_closedPoint_mem f hxU).ge
  rw [IsAffineOpen.fromSpec_top, Iso.eq_inv_comp, isoSpec_Spec_hom] at this
  rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc,
    germ_stalkClosedPointTo]
  simpa only [Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, Category.assoc,
    Hom.app_eq_appLE, Hom.appLE_map_assoc, Spec.map_comp_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T T' : Triplet f g
h : T = T'
⊢ Spec.map (Triplet.tensorCongr h).hom ≫ T.SpecTensorTo = T'.SpecTensorTo

Tactic:
subst h
  simp only [Triplet.tensorCongr_refl, Iso.refl_hom, Spec.map_id, Category.id_comp]

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

Goal state before:
pp: case a.inr.refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this✝¹ : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
this✝ : x ∈ closure (Set.range ⇑(Cover.pullbackHom 𝒰 f i))
this : (𝒰.f i) x ∈ closure (Set.range ⇑((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f))
⊢ (𝒰.f i) x ∈ closure (Set.range ⇑f)

Tactic:
exact closure_mono (Set.range_comp_subset_range _ _) this

Goal state after:
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)
this : QuasiSeparatedSpace ↥X
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
⊢ IsCompact ↑(⨆ i ∈ ↑s', X.basicOpen i)

Tactic:
simp only [Finset.mem_coe, Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk]

Goal state after:
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace ↥X
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
⊢ IsCompact (⋃ i ∈ s', ↑(X.basicOpen i))
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
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y),
    (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty f →
      (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty (f ≫ e.hom)

Tactic:
intro X Y Z e f ⟨hZ, hf⟩
    simpa [AffineTargetMorphismProperty.toProperty, IsAffine.of_isIso e.inv, hP.cancel_left_isIso]

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

Goal state before:
pp: case hs₂
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ ∀ i ∈ ⇑(ConcreteCategory.hom U.topIso.inv) '' s, IsAffineOpen ((↑U).basicOpen i)

Tactic:
rintro _ ⟨j, hj, rfl⟩
    rw [← (Scheme.Opens.ι _).isAffineOpen_iff_of_isOpenImmersion, Scheme.image_basicOpen]
    simpa [Scheme.Opens.toScheme_presheaf_obj] using hs₂ j hj

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this✝ : IsIso (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V =
    I.glueData.ι U
⊢ I.glueDataObjMap h ≫ I.glueData.ι V =
    𝟙 (I.glueData.U U) ≫
      inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
        I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V

Tactic:
simp_rw [← Category.assoc]

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this✝ : IsIso (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V =
    I.glueData.ι U
⊢ I.glueDataObjMap h ≫ I.glueData.ι V =
    𝟙 (I.glueData.U U) ≫
      ((inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫ I.glueDataT U V) ≫
          pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) ≫
        I.glueData.ι V
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
x : ↥I.subscheme
⊢ (I.subschemeIso.hom ≫ I.gluedTo) x = ↑x

Tactic:
change (I.gluedHomeo (I.gluedHomeo.symm x)).1 = x.1

Goal state after:
X : Scheme
I : X.IdealSheafData
x : ↥I.subscheme
⊢ ↑(I.gluedHomeo (I.gluedHomeo.symm x)) = ↑x
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case mpr
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
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f →
    ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
intro h U hU

Goal state after:
case mpr
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
h : affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
U : Y.Opens
hU : IsAffineOpen U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
⊢ app (toImage f) (imageι f ⁻¹ᵁ ↑U) =
    ((ker f).subschemeObjIso U).hom ≫
      CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f ↑U)) ⋯)

Tactic:
by
  have := ConcreteCategory.epi_of_surjective _ (f.ker.subschemeι_app_surjective U)
  rw [← cancel_epi (f.ker.subschemeι.app U), ← Scheme.Hom.comp_app,
    Scheme.Hom.congr_app f.toImage_imageι, f.ker.subschemeι_app,
    ← IsIso.eq_comp_inv, ← Functor.map_inv]
  simp only [Hom.comp_base, Opens.map_comp_obj, Category.assoc,
    Iso.inv_hom_id_assoc, eqToHom_op, inv_eqToHom]
  rw [← reassoc_of% CommRingCat.ofHom_comp, Ideal.Quotient.lift_comp_mk, CommRingCat.ofHom_hom,
    eqToHom_refl, CategoryTheory.Functor.map_id]
  exact (Category.comp_id _).symm

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

Goal state before:
pp: R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (Localization.awayMap f ↑r).Finite
this✝¹ : Algebra R S := f.toAlgebra
this✝ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
this : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
⊢ f.Finite

Tactic:
have : ∀ r : s, IsScalarTower R (Localization.Away (r : R)) (Localization.Away (f r)) :=
    fun r => IsScalarTower.of_algebraMap_eq'
      (IsLocalization.map_comp (Submonoid.powers (r : R)).le_comap_map).symm

Goal state after:
R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (Localization.awayMap f ↑r).Finite
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
⊢ f.Finite
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ LocallyOfFiniteType f ↔ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f

Tactic:
locallyOfFiniteType_iff,

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FiniteType) ↔
    affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: Z : Scheme
I : Z.IdealSheafData
⊢ Hom.ker (I.subschemeι ≫ inv (𝟙 Z)) = I

Tactic:
IsIso.inv_id,

Goal state after:
Z : Scheme
I : Z.IdealSheafData
⊢ Hom.ker (I.subschemeι ≫ 𝟙 Z) = I
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
this : IsClosedImmersion (Scheme.Hom.toImage f)
⊢ IsIso (Scheme.Hom.toImage f)

Tactic:
have : IsHomeomorph f.toImage :=
    isHomeomorph_iff_isEmbedding_surjective.mpr ⟨f.toImage.isEmbedding, by
      rw [← Set.range_eq_univ, ← f.toImage.isClosedEmbedding.isClosed_range.closure_eq]
      exact f.toImage.denseRange.closure_eq⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
this✝ : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph ⇑(Scheme.Hom.toImage f)
⊢ IsIso (Scheme.Hom.toImage f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
hY : IsAffine Y
this : IsAffine X
⊢ IsSeparated f

Tactic:
MorphismProperty.arrow_mk_iso_iff @IsSeparated (arrowIsoSpecΓOfIsAffine f)

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
hY : IsAffine Y
this : IsAffine X
⊢ IsSeparated (Spec.map (Scheme.Hom.appTop f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
⊢ IsImmersion (pullback.diagonal f)

Tactic:
let 𝒱 (i) := (pullback f (𝒰.f i)).affineCover

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun i ↦ (pullback f (𝒰.f i)).affineCover
⊢ IsImmersion (pullback.diagonal f)
Module: Mathlib.LinearAlgebra.Charpoly.BaseChange

Goal state before:
pp: R : Type u_3
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
b : Module.Basis I R M := Module.Free.chooseBasis R M
⊢ (toMatrix (Module.Basis.baseChange A b) (Module.Basis.baseChange A b)) (baseChange A f) =
    ((toMatrix b b) f).map ⇑(algebraMap R A)

Tactic:
ext i j

Goal state after:
R : Type u_3
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
b : Module.Basis I R M := Module.Free.chooseBasis R M
i j : I
⊢ (toMatrix (Module.Basis.baseChange A b) (Module.Basis.baseChange A b)) (baseChange A f) i j =
    ((toMatrix b b) f).map (⇑(algebraMap R A)) i j
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑f
𝒰 : Y.OpenCover := Y.affineCover
⊢ autoParam (IsClosedImmersion (pullback.diagonal f)) IsSeparated.isClosedImmersion_diagonal._autoParam

Tactic:
let 𝒱 (i) := (pullback f (𝒰.f i)).affineCover

Goal state after:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑f
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun i ↦ (pullback f (𝒰.f i)).affineCover
⊢ autoParam (IsClosedImmersion (pullback.diagonal f)) IsSeparated.isClosedImmersion_diagonal._autoParam