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

Goal state before:
pp: R S T : Type u_4
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R T).EssFiniteType
⊢ (algebraMap S (TensorProduct R S T)).EssFiniteType

Tactic:
rw [essFiniteType_algebraMap] at h ⊢

Goal state after:
R S T : Type u_4
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : Algebra.EssFiniteType R T
⊢ Algebra.EssFiniteType S (TensorProduct R S T)
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
h :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
U : Y.Opens
hU : IsAffineOpen U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
f.app_eq_appLE

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 :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
U : Y.Opens
hU : IsAffineOpen U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
h : Function.Surjective ⇑(ConcreteCategory.hom f)
x : ↥(Spec S)
⊢ RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ Function.Surjective ⇑f

Tactic:
exact RingHom.surjective_respectsIso

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
e_2✝ : ↥s = ↑↑s
C : ↥s
I : Ideal R := ⋯
f : R ⧸ I := ⋯
⊢ Set.range
      (comap
        ((Pi.evalRingHom (fun i ↦ Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))
              C).comp
          (algebraMap R ((i : ↥s) → Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))))) =
    comap (Ideal.Quotient.mk I) '' Set.range (comap (algebraMap (R ⧸ I) (Localization.Away f)))

Tactic:
← Set.range_comp

Goal state after:
R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
e_2✝ : ↥s = ↑↑s
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C).g)
f : R ⧸ I := (Ideal.Quotient.mk I) (↑C).f
⊢ Set.range
      (comap
        ((Pi.evalRingHom (fun i ↦ Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))
              C).comp
          (algebraMap R ((i : ↥s) → Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i).g))) (↑i).f))))) =
    Set.range (comap (Ideal.Quotient.mk I) ∘ comap (algebraMap (R ⧸ I) (Localization.Away f)))
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
S : ConstructibleSetData R[X]
hs : IsConstructible S.toSet
T : ConstructibleSetData R
hT : comap Polynomial.C '' S.toSet = T.toSet
⊢ IsConstructible T.toSet

Tactic:
exact T.isConstructible_toSet

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

Goal state before:
pp: case inr
Y : Scheme
inst✝ : Subsingleton ↥Y
R : CommRingCat
f : Spec R ⟶ Y
g : Y ⟶ Spec R
hg : g ≫ f = 𝟙 Y
this :
  ∀ {Y : Scheme} [Subsingleton ↥Y] (R : CommRingCat) (f : Spec R ⟶ Y) (g : Y ⟶ Spec R),
    g ≫ f = 𝟙 Y → (∃ S, Y = Spec S) → IsClosedImmersion g
hY : ¬∃ S, Y = Spec S
inst : Subsingleton ↥(Spec Γ(Y, ⊤))
⊢ IsClosedImmersion g

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion (Scheme.isoSpec Y).inv]

Goal state after:
case inr
Y : Scheme
inst✝ : Subsingleton ↥Y
R : CommRingCat
f : Spec R ⟶ Y
g : Y ⟶ Spec R
hg : g ≫ f = 𝟙 Y
this :
  ∀ {Y : Scheme} [Subsingleton ↥Y] (R : CommRingCat) (f : Spec R ⟶ Y) (g : Y ⟶ Spec R),
    g ≫ f = 𝟙 Y → (∃ S, Y = Spec S) → IsClosedImmersion g
hY : ¬∃ S, Y = Spec S
inst : Subsingleton ↥(Spec Γ(Y, ⊤))
⊢ IsClosedImmersion (Y.isoSpec.inv ≫ g)
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
⊢ IsNilpotent ((algebraMap A (A ⊗[R] I.ResidueField)) f) ↔
    ∀ i < Module.finrank R A, (LinearMap.charpoly ((Algebra.lmul R A) f)).coeff i ∈ I

Tactic:
by
  cases subsingleton_or_nontrivial R
  · have := (algebraMap R (A ⊗[R] I.ResidueField)).codomain_trivial
    simp [Subsingleton.elim I ⊤, Subsingleton.elim (f ⊗ₜ[R] (1 : I.ResidueField)) 0]
  have : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A := by
    rw [Module.finrank_tensorProduct, Module.finrank_self, one_mul]
  rw [← IsNilpotent.map_iff (Algebra.TensorProduct.comm R A I.ResidueField).injective]
  simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
    Algebra.coe_lmul_eq_mul, Algebra.TensorProduct.comm_tmul]
  rw [← IsNilpotent.map_iff (Algebra.lmul_injective (R := I.ResidueField)),
    LinearMap.isNilpotent_iff_charpoly, ← Algebra.baseChange_lmul, LinearMap.charpoly_baseChange,
    this]
  simp_rw [← ((LinearMap.mul R A) f).charpoly_natDegree]
  constructor
  · intro e i hi
    replace e := congr(($e).coeff i)
    simpa only [Algebra.coe_lmul_eq_mul, coeff_map, coeff_X_pow, hi.ne, ↓reduceIte,
      ← RingHom.mem_ker, Ideal.ker_algebraMap_residueField] using e
  · intro H
    ext i
    obtain (hi | hi) := eq_or_ne i ((LinearMap.mul R A) f).charpoly.natDegree
    · simp only [Algebra.coe_lmul_eq_mul, hi, coeff_map, coeff_X_pow, ↓reduceIte]
      rw [← Polynomial.leadingCoeff, ((LinearMap.mul R A) f).charpoly_monic, map_one]
    obtain (hi | hi) := lt_or_gt_of_ne hi
    · simpa [hi.ne, ← RingHom.mem_ker, Ideal.ker_algebraMap_residueField] using H i hi
    · simp [hi.ne', coeff_eq_zero_of_natDegree_lt hi]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: case refine_2
X : Scheme
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)
i : 𝒰.I₀
x : ↥(𝒰.X i)
⊢ IsOpen {(𝒰.f i) x}

Tactic:
simpa using (𝒰.f i).isOpenEmbedding.isOpenMap _ (isOpen_discrete {x})

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : Finite ↑(irreducibleComponents ↥Y)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := fun Z ↦ Y.presheaf.stalk ⋯.genericPoint
Z : ↑(irreducibleComponents ↥Y)
⊢ closure {⋯.genericPoint} ∈ irreducibleComponents ↥Y

Tactic:
rw [Z.property.1.closure_genericPoint (isClosed_of_mem_irreducibleComponents _ Z.property)]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : Finite ↑(irreducibleComponents ↥Y)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := fun Z ↦ Y.presheaf.stalk ⋯.genericPoint
Z : ↑(irreducibleComponents ↥Y)
⊢ ↑Z ∈ irreducibleComponents ↥Y
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
hU : IsAffineOpen U
⊢ Function.Injective ⇑(ConcreteCategory.hom (app f U))

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
⊢ Function.Injective ⇑(ConcreteCategory.hom (app f U))

Tactic:
· rw [RingHom.injective_iff_ker_eq_bot, ← f.ker_apply ⟨U, hU⟩, f.ker_eq_bot]
    simp

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
⊢ Function.Injective ⇑(ConcreteCategory.hom (app f U))
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtSource (topologically @IsOpenMap).universally

Tactic:
exact universally_isZariskiLocalAtSource _

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

Goal state before:
pp: ⊢ @GeometricallyIntegral = @GeometricallyReduced ⊓ @GeometricallyIrreducible

Tactic:
eq_geometrically,

Goal state after:
⊢ geometrically IsIntegral = @GeometricallyReduced ⊓ @GeometricallyIrreducible
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: case inr
X Y✝ : Scheme
f✝ : X ⟶ Y✝
Y : Scheme
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
S : CommRingCat
f : Spec S ⟶ Y
this :
  ∀ {Y : Scheme} [IsIntegral Y] [Subsingleton ↥Y] (f : Spec S ⟶ Y), (∃ K, Y = Spec K ∧ IsField ↑K) → UniversallyOpen f
hY : ¬∃ K, Y = Spec K ∧ IsField ↑K
⊢ UniversallyOpen f

Tactic:
have inst : Subsingleton (Spec Γ(Y, ⊤)) := Y.isoSpec.inv.homeomorph.subsingleton

Goal state after:
case inr
X Y✝ : Scheme
f✝ : X ⟶ Y✝
Y : Scheme
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
S : CommRingCat
f : Spec S ⟶ Y
this :
  ∀ {Y : Scheme} [IsIntegral Y] [Subsingleton ↥Y] (f : Spec S ⟶ Y), (∃ K, Y = Spec K ∧ IsField ↑K) → UniversallyOpen f
hY : ¬∃ K, Y = Spec K ∧ IsField ↑K
inst : Subsingleton ↥(Spec Γ(Y, ⊤))
⊢ UniversallyOpen f
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: ⊢ HasAffineProperty @IsFinite fun X x f x_1 ↦ IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Tactic:
change HasAffineProperty @IsFinite (affineAnd RingHom.Finite)

Goal state after:
⊢ HasAffineProperty (@IsFinite) (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ RingHom.Finite)
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f

Tactic:
HasAffineProperty.iff_of_isAffine (P := @IsClosedImmersion),

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) ↔ IsFinite f ∧ Mono f
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
⊢ GeometricallyIrreducible (𝔸(n; S) ↘ S)

Tactic:
geometricallyIrreducible_iff

Goal state after:
n : Type u
S : Scheme
⊢ geometrically (fun x ↦ IrreducibleSpace ↥x) (𝔸(n; S) ↘ S)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
H : ¬∃ i, (e.val i).Monic ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
i : Fin n
hi : e.val i ≠ 0
i_min : ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
⊢ { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {(e.val i).leadingCoeff}))) ∘ e.val }.degree < v

Tactic:
rw [hv]
      refine .left _ _ (lt_of_le_of_ne ?_ ?_)
      · intro j; simpa using degree_map_le
      simp only [coe_mapRingHom, ne_eq]
      intro h_eq
      replace h_eq := congr_fun h_eq i
      simp only [Ideal.Quotient.algebraMap_eq, comp_apply, degree_map_eq_iff,
        Ideal.Quotient.mk_singleton_self, ne_eq, not_true_eq_false, false_or] at h_eq
      exact hi h_eq

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

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
G : X.Opens ⥤ Y.Opens :=
  { obj := fun U ↦ g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map := fun {X_1 Y_1} h ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
i : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ D.obj (unop i) ≤ iSup D.obj

Tactic:
exact le_iSup D.obj i.unop

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

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
G : X.Opens ⥤ Y.Opens :=
  { obj := fun U ↦ g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map := fun {X_1 Y_1} h ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
i : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ D.obj (unop i) ≤ iX ⁻¹ᵁ US

Tactic:
by grw [← hUSX, ← h]; exact le_iSup D.obj i.unop

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
⊢ EqOn (⇑(D.restrict h)) 0 Vᶜ

Tactic:
by
  intro _ hx
  simp_all

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IrreducibleSpace ↥X
U : X.Opens
h : Nonempty ↥↑U
⊢ (Set.univ ∩ ↑U).Nonempty

Tactic:
simpa using h

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ nonZeroDivisors ↑R = (genericPoint ↥(Spec R)).asIdeal.primeCompl

Tactic:
genericPoint_eq_bot_of_affine

Goal state after:
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ nonZeroDivisors ↑R = ⊥.asIdeal.primeCompl
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X✝ : Scheme
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty ↥↑U
⊢ (Set.univ ∩ ↑U).Nonempty

Tactic:
simpa using h

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: case e'_3
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↥↑U
⊢ nonZeroDivisors ↑Γ(X, U) = (genericPoint ↥(Spec Γ(X, U))).asIdeal.primeCompl

Tactic:
genericPoint_eq_bot_of_affine

Goal state after:
case e'_3
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↥↑U
⊢ nonZeroDivisors ↑Γ(X, U) = ⊥.asIdeal.primeCompl
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y S : Scheme
inst✝² : X.Over S
inst✝¹ : Y.Over S
f : X.PartialMap Y
inst✝ : RationalMap.IsOver S f.toRationalMap
⊢ ∃ U, ∃ (hU : Dense ↑U) (hU' : U ≤ f.domain), IsOver S (f.restrict U hU hU')

Tactic:
obtain ⟨f', hf₁, hf₂⟩ := RationalMap.IsOver.exists_partialMap_over (S := S) (f := f.toRationalMap)

Goal state after:
X Y S : Scheme
inst✝² : X.Over S
inst✝¹ : Y.Over S
f : X.PartialMap Y
inst✝ : RationalMap.IsOver S f.toRationalMap
f' : X.PartialMap Y
hf₁ : IsOver S f'
hf₂ : f'.toRationalMap = f.toRationalMap
⊢ ∃ U, ∃ (hU : Dense ↑U) (hU' : U ≤ f.domain), IsOver S (f.restrict U hU hU')
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
ext
  · simp_rw [comp_domain, comp_hom, ← Category.assoc, Hom.comp_preimage, Hom.inv_preimage,
      ← Hom.comp_image, Hom.isoImage_hom_ι, Hom.comp_image, image_morphismRestrict_preimage]
  · dsimp
    simp_rw [morphismRestrict_comp, morphismRestrict_ι_image_ι_isoImage_inv_assoc,
      Hom.comp_preimage, Category.assoc]
    conv_lhs => rw [← Category.assoc]
    conv_rhs => rw [← Category.assoc, ← Category.assoc, ← Category.assoc]
    congr 1
    simp [← cancel_mono (Opens.ι _)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝¹ : Category.{u_2, u_1} 𝒰.I₀
inst✝ : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
i j : 𝒰.I₀
hij : i ⟶ j
⊢ IsOpenImmersion (d.functor.map hij)

Tactic:
apply MorphismProperty.of_isPullback (d.equifibered hij).flip

Goal state after:
S : Scheme
𝒰 : S.OpenCover
inst✝¹ : Category.{u_2, u_1} 𝒰.I₀
inst✝ : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
i j : 𝒰.I₀
hij : i ⟶ j
⊢ IsOpenImmersion ((functorOfLocallyDirected 𝒰).map hij)
Module: Mathlib.AlgebraicGeometry.Cover.Over

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝³ : W.Over S
inst✝² : X.Over S
inst✝¹ : Cover.Over S 𝒰
inst✝ : Hom.IsOver f S
j :
  { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
      f := fun x ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }.I₀
⊢ P (Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f j) S)))

Tactic:
rw [← Over.forget_map, ← PreservesPullback.iso_hom_fst, P.cancel_left_of_respectsIso]

Goal state after:
case refine_2
P : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝³ : W.Over S
inst✝² : X.Over S
inst✝¹ : Cover.Over S 𝒰
inst✝ : Hom.IsOver f S
j :
  { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
      f := fun x ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }.I₀
⊢ P (pullback.fst ((Over.forget S).map (Hom.asOver f S)) ((Over.forget S).map (Hom.asOver (𝒰.f j) S)))
Module: Mathlib.AlgebraicGeometry.Cover.Over

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
S : Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝⁶ : W.Over S
inst✝⁵ : X.Over S
inst✝⁴ : Cover.Over S 𝒰
inst✝³ : Hom.IsOver f S
Q : MorphismProperty Scheme
inst✝² : Q.HasOfPostcompProperty Q
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
x : ↥W
⊢ ∃ i,
    x ∈
      Set.range
        ⇑({ I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left,
                f := fun x ↦ (pullback.fst (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left }.f
            i)

Tactic:
obtain ⟨i, hy⟩ := Cover.exists_eq (𝒰.pullback₁ f) x
      use i
      exact (mem_range_iff_of_surjective ((𝒰.pullback₁ f).f i) _
        ((PreservesPullback.iso (MorphismProperty.Over.forget Q _ _ ⋙ Over.forget S)
          (f.asOverProp S) ((𝒰.f _).asOverProp S)).inv)
        (PreservesPullback.iso_inv_fst _ _ _) x).mp hy

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, ↑t = U
H : ∀ t ∈ s, IsCompactOpenCovered f ↑t
t : Finset ↑s
ht : U ⊆ ⋃ i ∈ t, ↑↑i
⊢ IsCompactOpenCovered f U

Tactic:
refine of_biUnion_eq_of_finite (SetLike.coe '' (t.image Subtype.val : Set (Opens S))) ?_ ?_ ?_

Goal state after:
case refine_1
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, ↑t = U
H : ∀ t ∈ s, IsCompactOpenCovered f ↑t
t : Finset ↑s
ht : U ⊆ ⋃ i ∈ t, ↑↑i
⊢ ⋃ t_1 ∈ SetLike.coe '' ↑(Finset.image Subtype.val t), t_1 = U

case refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, ↑t = U
H : ∀ t ∈ s, IsCompactOpenCovered f ↑t
t : Finset ↑s
ht : U ⊆ ⋃ i ∈ t, ↑↑i
⊢ (SetLike.coe '' ↑(Finset.image Subtype.val t)).Finite

case refine_3
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, ↑t = U
H : ∀ t ∈ s, IsCompactOpenCovered f ↑t
t : Finset ↑s
ht : U ⊆ ⋃ i ∈ t, ↑↑i
⊢ ∀ t_1 ∈ SetLike.coe '' ↑(Finset.image Subtype.val t), IsCompactOpenCovered f t_1
Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: C✝ : Type u_1
inst✝⁶ : Category.{v_1, u_1} C✝
D✝ : Type u_2
inst✝⁵ : Category.{v_2, u_2} D✝
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst✝² : EffectiveEpi f
F : C ⥤ D
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ ∀ (j : WalkingCospan),
    ((Cone.postcompose
                  (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
                      (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left))
                      (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
              (F.mapCone c)).π.app
        j =
      (Iso.refl
            ((Cone.postcompose
                    (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
                        (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left))
                        (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
                (F.mapCone c)).pt).hom ≫
        (PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯).π.app j

Tactic:
rintro (_ | _ | _) <;> cat_disch

Goal state after: