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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : IsFinite f
inst✝ : LocallyOfFinitePresentation f
⊢ IsLocallyConstant (finrank f)

Tactic:
by
  wlog hY : ∃ R, Y = Spec R
  · rw [IsLocallyConstant.iff_exists_open]
    intro y
    obtain ⟨R, g, _, x, rfl⟩ := Y.exists_Spec_apply_eq y
    simp_rw [IsLocallyConstant.iff_exists_open] at this
    obtain ⟨U, hU, hxU, H⟩ := this (pullback.snd f g) ⟨_, rfl⟩ x
    refine ⟨g ''ᵁ ⟨U, hU⟩, (g ''ᵁ ⟨U, hU⟩).2, ⟨x, hxU, rfl⟩, fun y ↦ ?_⟩
    rintro ⟨y', (hyU : y' ∈ U), (rfl : g y' = y)⟩
    rw [← finrank_pullback_snd _ g, ← finrank_pullback_snd _ g]
    exact H y' hyU
  obtain ⟨R, rfl⟩ := hY
  wlog hX : ∃ S, X = Spec S
  · have _ : IsAffine X := isAffine_of_isAffineHom f
    rw [← finrank_comp_left_of_isIso X.isoSpec.inv]
    exact this _ _ ⟨_, rfl⟩
  obtain ⟨S, rfl⟩ := hX
  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
  simp only [Flat.SpecMap_iff, IsFinite.SpecMap_iff, LocallyOfFinitePresentation.SpecMap_iff] at *
  rw [finrank_SpecMap_eq_finrank ‹_› ‹_›]
  algebraize [φ.hom]
  have := Module.FinitePresentation.of_finite_of_finitePresentation
  exact Module.isLocallyConstant_rankAtStalk

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

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := ⋯
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ Module.rankAtStalk ↑S = 1

Tactic:
finrank_SpecMap_eq_finrank ‹_› ‹_›

Goal state after:
R S : CommRingCat
φ : R ⟶ S
h : (CommRingCat.Hom.hom φ).finrank = 1
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ Module.rankAtStalk ↑S = 1
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → ↑(R i)))
inst✝¹ : IsImmersion g
inst✝ : CompactSpace ↥V
hU' : f ≫ g = sigmaSpec R
this✝ : Scheme.Hom.coborderRange g = ⊤
this : IsClosedImmersion g
⊢ IsIso g

Tactic:
obtain ⟨I, e, rfl⟩ := IsClosedImmersion.Spec_iff.mp this

Goal state after:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
inst✝¹ : CompactSpace ↥V
I : Ideal ↑(CommRingCat.of ((i : ι) → ↑(R i)))
e : V ≅ Spec (CommRingCat.of (↑(CommRingCat.of ((i : ι) → ↑(R i))) ⧸ I))
inst✝ : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
this✝ : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
⊢ IsIso (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
g : (j₀ : 𝒰.I₀) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.X j₀
hg :
  ∀ (j₀ : 𝒰.I₀) (x : { i // j i = j₀ }),
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ ↑(R ↑x)) x)) ≫ g j₀ = IsOpenImmersion.lift (𝒰.f j₀) (f ↑x) ⋯
R' : 𝒰.I₀ → CommRingCat := fun j₀ ↦ CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))
e : ((i : ι) → ↑(R i)) ≃+* ((j₀ : 𝒰.I₀) → ↑(R' j₀)) :=
  { toFun := fun f x i ↦ f ↑i, invFun := fun f i ↦ f (j i) ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯ }
i : ι
this :
  (Pi.evalRingHom (fun x ↦ ↑(R x)) i).comp e.symm.toRingHom =
    (Pi.evalRingHom (fun i_1 ↦ ↑(R ↑i_1)) ⟨i, ⋯⟩).comp (Pi.evalRingHom (fun x ↦ ↑(R' x)) (j i))
⊢ pointsPi R X (Spec.map (CommRingCat.ofHom e.symm.toRingHom) ≫ inv (sigmaSpec R') ≫ Sigma.desc fun j₀ ↦ g j₀ ≫ 𝒰.f j₀)
      i =
    f i

Tactic:
pointsPi,

Goal state after:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
g : (j₀ : 𝒰.I₀) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.X j₀
hg :
  ∀ (j₀ : 𝒰.I₀) (x : { i // j i = j₀ }),
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ ↑(R ↑x)) x)) ≫ g j₀ = IsOpenImmersion.lift (𝒰.f j₀) (f ↑x) ⋯
R' : 𝒰.I₀ → CommRingCat := fun j₀ ↦ CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))
e : ((i : ι) → ↑(R i)) ≃+* ((j₀ : 𝒰.I₀) → ↑(R' j₀)) :=
  { toFun := fun f x i ↦ f ↑i, invFun := fun f i ↦ f (j i) ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯ }
i : ι
this :
  (Pi.evalRingHom (fun x ↦ ↑(R x)) i).comp e.symm.toRingHom =
    (Pi.evalRingHom (fun i_1 ↦ ↑(R ↑i_1)) ⟨i, ⋯⟩).comp (Pi.evalRingHom (fun x ↦ ↑(R' x)) (j i))
⊢ (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ ↑(R x)) i)) ≫
      Spec.map (CommRingCat.ofHom e.symm.toRingHom) ≫ inv (sigmaSpec R') ≫ Sigma.desc fun j₀ ↦ g j₀ ≫ 𝒰.f j₀) =
    f i
Module: Mathlib.RingTheory.GradedAlgebra.FiniteType

Goal state before:
pp: case neg
S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
n : S → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
i : S
hi : i ∈ ↑s
hi0 : ¬n i = 0
⊢ i ∈ ↑(Algebra.adjoin ↥(𝒜 0) ↑({x ∈ s | n x ≠ 0}))

Tactic:
exact Algebra.subset_adjoin (by simpa [hi0] using hi)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f✝ : X ⟶ Y
g : Y ⟶ Z
inst✝² : IsOpenImmersion f✝
inst✝¹ : IsOpenImmersion g
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ restrict (unit Y.ringCatSheaf) f ≅ unit X.ringCatSheaf

Tactic:
by
  refine (fullyFaithfulForget _).preimageIso <| PresheafOfModules.isoMk (fun U ↦ ?_) ?_
  · refine ModuleCat.isoMk
      ((forget₂ CommRingCat RingCat ⋙ forget₂ _ Ab).mapIso (f.appIso U.unop)) ?_
    intro (r : Γ(X, U.unop))
    ext (x : Γ(Y, f ''ᵁ U.unop))
    change r * (f.appIso U.unop).hom x = (f.appIso U.unop).hom ((f.appIso U.unop).inv r * x)
    simp
  · intro U V g
    have : Y.presheaf.map (homOfLE (by grw [leOfHom g.unop])).op ≫
        (f.appIso _).hom = (f.appIso U.unop).hom ≫ X.presheaf.map g := by
      simp [Hom.appIso_hom']
    ext x
    exact congr($(this) x)

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case e'_2
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ Localization.mk (↑c1.den * ↑c3.num + ↑c3.den * ↑c1.num) ⟨↑c1.den * ↑c3.den, ⋯⟩ =
    Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ + Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩

Tactic:
rw [Localization.add_mk]

Goal state after:
case e'_2
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ Localization.mk (↑c1.den * ↑c3.num + ↑c3.den * ↑c1.num) ⟨↑c1.den * ↑c3.den, ⋯⟩ =
    Localization.mk (↑⟨↑c1.den, ⋯⟩ * ↑c3.num + ↑⟨↑c3.den, ⋯⟩ * ↑c1.num) (⟨↑c1.den, ⋯⟩ * ⟨↑c3.den, ⋯⟩)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case e'_3
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ Localization.mk (↑c2.den * ↑c4.num + ↑c4.den * ↑c2.num) ⟨↑c2.den * ↑c4.den, ⋯⟩ =
    Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩ + Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩

Tactic:
rw [Localization.add_mk]

Goal state after:
case e'_3
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ Localization.mk (↑c2.den * ↑c4.num + ↑c4.den * ↑c2.num) ⟨↑c2.den * ↑c4.den, ⋯⟩ =
    Localization.mk (↑⟨↑c2.den, ⋯⟩ * ↑c4.num + ↑⟨↑c4.den, ⋯⟩ * ↑c2.num) (⟨↑c2.den, ⋯⟩ * ⟨↑c4.den, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
⊢ (∀ (i : ℕ),
      HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈
        q.asIdeal) ↔
    ∀ (i : ℕ),
      Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩ ∈ ⇑(algebraMap (A⁰_ f) (Localization.Away f)) '' {s | s ∈ q.asIdeal}

Tactic:
constructor <;> intro h i <;> specialize h i

Goal state after:
case mp
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
h :
  HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
⊢ Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩ ∈ ⇑(algebraMap (A⁰_ f) (Localization.Away f)) '' {s | s ∈ q.asIdeal}

case mpr
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
i : ℕ
h : Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩ ∈ ⇑(algebraMap (A⁰_ f) (Localization.Away f)) '' {s | s ∈ q.asIdeal}
⊢ HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ a ∈ carrier f_deg q ↔
    HomogeneousLocalization.mk { deg := m * n, num := ⟨(proj 𝒜 n) a ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal

Tactic:
refine ⟨fun h ↦ h n, fun h i ↦ if hi : i = n then hi ▸ h else ?_⟩

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
n : ℕ
hn : a ∈ 𝒜 n
h :
  HomogeneousLocalization.mk { deg := m * n, num := ⟨(proj 𝒜 n) a ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
i : ℕ
hi : ¬i = n
⊢ HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : SetLike σ A
inst✝¹¹ : AddSubgroupClass σ A
inst✝¹⁰ : AddCommMonoid ι
inst✝⁹ : DecidableEq ι
𝒜 : ι → σ
inst✝⁸ : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst✝⁷ : CommRing B
inst✝⁶ : SetLike τ B
inst✝⁵ : AddSubgroupClass τ B
ℬ : ι → τ
inst✝⁴ : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst✝³ : CommRing C
inst✝² : SetLike ψ C
inst✝¹ : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst✝ : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
⊢ Quotient.map' (fun x ↦ { deg := x.deg, num := ⟨g ↑x.num, ⋯⟩, den := ⟨g ↑x.den, ⋯⟩, den_mem := ⋯ }) ⋯ 0 = 0

Tactic:
by simp only [← mk_zero (𝒜 := 𝒜), Quotient.map'_mk'', deg_zero,
    num_zero, ZeroMemClass.coe_zero, map_zero, den_zero, map_one]; rfl

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
⊢ g ^ e * f ^ (2 * e + d) ∈ 𝒜 ((d + e) • (d + e))

Tactic:
convert!
        SetLike.mul_mem_graded (SetLike.pow_mem_graded e hg)
          (SetLike.pow_mem_graded (2 * e + d) hf) using 2

Goal state after:
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
⊢ (d + e) • (d + e) = e • e + (2 * e + d) • d
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec R).Modules
f : modulesSpecToSheaf.obj M ⟶ modulesSpecToSheaf.obj N
U : (Opens ↥(Spec R))ᵒᵖ
t : ↑((Spec R).ringCatSheaf.obj.obj U)
⊢ ∀ (x : ↑(M.val.1 U)),
    (ModuleCat.Hom.hom (f.hom.app U)).toFun (t • x) =
      (RingHom.id ↑((Spec R).ringCatSheaf.obj.obj U)) t • (ModuleCat.Hom.hom (f.hom.app U)).toFun x

Tactic:
m

Goal state after:
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec R).Modules
f : modulesSpecToSheaf.obj M ⟶ modulesSpecToSheaf.obj N
U : (Opens ↥(Spec R))ᵒᵖ
t : ↑((Spec R).ringCatSheaf.obj.obj U)
m : ↑(M.val.1 U)
⊢ (ModuleCat.Hom.hom (f.hom.app U)).toFun (t • m) =
    (RingHom.id ↑((Spec R).ringCatSheaf.obj.obj U)) t • (ModuleCat.Hom.hom (f.hom.app U)).toFun m
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
⊢ Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d) ∈
    Subalgebra.toSubmodule
      (Algebra.adjoin ↥(𝒜 0)
        {x |
          ∃ a ai,
            ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x})

Tactic:
apply (Algebra.adjoin (𝒜 0) _).mul_mem

Goal state after:
case hx
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
⊢ Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ ∈
    Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}

case hy
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
⊢ ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d) ∈
    Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A σ : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
⊢ map (GradedRingHom.id 𝒜) ⋯ = 𝟙 (Proj 𝒜)

Tactic:
refine (affineOpenCover _).openCover.hom_ext _ _ fun s ↦ ?_
  convert! awayι_comp_map (.id 𝒜) _ _ _ s.2.2 using 1
  simp

Goal state after:
Module: Mathlib.RingTheory.Valuation.Integral

Goal state before:
pp: case neg
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf : ∑ i ∈ Finset.range f.natDegree, (algebraMap O R) (f.coeff i) * x ^ i = -x ^ f.natDegree
⊢ v x ≤ 1

Tactic:
apply_fun v at hf

Goal state after:
case neg
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf : v (∑ i ∈ Finset.range f.natDegree, (algebraMap O R) (f.coeff i) * x ^ i) = v (-x ^ f.natDegree)
⊢ v x ≤ 1
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1
X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
I : Type u
W : I → TopologicalSpace.Opens ↥X
cov : (Opens.grothendieckTopology ↥X).CoversTop W
pres : (i : I) → (SheafOfModules.over M (W i)).Presentation
κ : I → Set (TopologicalSpace.Opens ↥X)
hsub : ∀ (i : I), κ i ⊆ X.affineOpens
heq : ∀ (i : I), W i = sSup (κ i)
i : (i : I) × ↑(κ i)
u : ↑↑i.snd ⟶ ↑(W i.fst) := X.homOfLE ⋯
this : PreservesColimitsOfSize.{u, u, u, u, u + 1, u + 1} (restrictFunctor u)
⊢ SheafOfModules.Presentation (M.restrict (Opens.ι ((fun j ↦ ↑j.snd) i)))

Tactic:
let F := (overEquiv (W i.1)).functor ⋙ restrictFunctor u

Goal state after:
case refine_1
X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
I : Type u
W : I → TopologicalSpace.Opens ↥X
cov : (Opens.grothendieckTopology ↥X).CoversTop W
pres : (i : I) → (SheafOfModules.over M (W i)).Presentation
κ : I → Set (TopologicalSpace.Opens ↥X)
hsub : ∀ (i : I), κ i ⊆ X.affineOpens
heq : ∀ (i : I), W i = sSup (κ i)
i : (i : I) × ↑(κ i)
u : ↑↑i.snd ⟶ ↑(W i.fst) := X.homOfLE ⋯
this : PreservesColimitsOfSize.{u, u, u, u, u + 1, u + 1} (restrictFunctor u)
F : SheafOfModules (Sheaf.over X.ringCatSheaf (W i.fst)) ⥤ (↑↑i.snd).Modules :=
  (overEquiv (W i.fst)).functor ⋙ restrictFunctor u
⊢ SheafOfModules.Presentation (M.restrict (Opens.ι ((fun j ↦ ↑j.snd) i)))
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ ValuativeCriterion f ↔ Existence f ∧ Uniqueness f

Tactic:
by
  change (∀ _, _) ↔ (∀ _, _) ∧ (∀ _, _)
  simp_rw [← forall_and, unique_iff_subsingleton_and_nonempty, and_comm, CommSq.HasLift.iff]

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

Goal state before:
pp: S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
⊢ ∃ ι U f,
    Sieve.ofArrows (fun i ↦ (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj (U i)) f ∈
      (smallGrothendieckTopology P S) X

Tactic:
by
    let 𝒰 := affineOpenCover X.left
    let 𝒱 : Cover (precoverage P) X.left :=
      𝒰.openCover.changeProp (fun _ ↦ IsZariskiLocalAtSource.of_isOpenImmersion _)
    let _ (i : 𝒱.I₀) : (𝒱.X i).Over S := ⟨𝒰.f i ≫ X.hom⟩
    let : Cover.Over S 𝒱 := { isOver_map _ := ⟨rfl⟩ }
    refine ⟨𝒰.I₀, fun i ↦ affineOverMk (𝒰.f i ≫ X.hom)
      (P.comp_mem _ _ (IsZariskiLocalAtSource.of_isOpenImmersion (𝒰.f i)) X.prop),
      fun i ↦ CostructuredArrow.homMk (𝒰.f i) (by simp), ?_⟩
    rw [Scheme.mem_smallGrothendieckTopology]
    exact ⟨𝒱, inferInstance, fun i ↦ P.comp_mem _ _ (𝒱.map_prop i) X.prop,
      fun _ _ ⟨i⟩ ↦ (Sieve.mem_ofArrows_iff ..).mpr ⟨i, 𝟙 _, by cat_disch⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : EffectiveEpiStruct f
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateSingleton f).arrows T.hom
F : D ⥤ C := (Sieve.generateSingleton f).arrows.diagram
S : Cocone (Sieve.generateSingleton f).arrows.diagram
⊢ ∀ (m : (Sieve.generateSingleton f).arrows.cocone.pt ⟶ S.pt),
    (∀ (j : (Sieve.generateSingleton f).arrows.category),
        (Sieve.generateSingleton f).arrows.cocone.ι.app j ≫ m = S.ι.app j) →
      m = Hf.desc (S.ι.app { obj := Over.mk f, property := ⋯ }) ⋯

Tactic:
m

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : EffectiveEpiStruct f
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateSingleton f).arrows T.hom
F : D ⥤ C := (Sieve.generateSingleton f).arrows.diagram
S : Cocone (Sieve.generateSingleton f).arrows.diagram
m : (Sieve.generateSingleton f).arrows.cocone.pt ⟶ S.pt
⊢ (∀ (j : (Sieve.generateSingleton f).arrows.category),
      (Sieve.generateSingleton f).arrows.cocone.ι.app j ≫ m = S.ι.app j) →
    m = Hf.desc (S.ι.app { obj := Over.mk f, property := ⋯ }) ⋯
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
⊢ ∀ {Y Z : C} {f : Y ⟶ B}, (∃ a g, g ≫ π a = f) → ∀ (g : Z ⟶ Y), ∃ a g_1, g_1 ≫ π a = g ≫ f

Tactic:
rintro Y₁ Y₂ g₁ ⟨a, q, rfl⟩ e
    exact ⟨a, e ≫ q, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamilyStruct X π
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
⊢ ∀ (m : (Sieve.generateFamily X π).arrows.cocone.pt ⟶ S.pt),
    (∀ (j : (Sieve.generateFamily X π).arrows.category),
        (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫ m = S.ι.app j) →
      m = H.desc (fun a ↦ S.ι.app { obj := Over.mk (π a), property := ⋯ }) ⋯

Tactic:
m

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamilyStruct X π
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
m : (Sieve.generateFamily X π).arrows.cocone.pt ⟶ S.pt
⊢ (∀ (j : (Sieve.generateFamily X π).arrows.category),
      (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫ m = S.ι.app j) →
    m = H.desc (fun a ↦ S.ι.app { obj := Over.mk (π a), property := ⋯ }) ⋯