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

Goal state before:
pp: case refine_2
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
U : X.Opensᵒᵖ
x : ↑(X.ringCatSheaf.obj.obj U)
⊢ (RingCat.Hom.hom
        (({
                  hom :=
                    Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
                      (forget₂ CommRingCat RingCat) }.hom ≫
              (Hom.opensFunctor f).op.whiskerLeft (Hom.toRingCatSheafHom f).hom ≫
                Functor.whiskerRight (NatTrans.op ⋯.adjunction.unit) X.ringCatSheaf.obj).app
          U))
      x =
    (RingCat.Hom.hom ((𝟙 X.ringCatSheaf.obj).app U)) x

Tactic:
have : (f.appIso U.unop).inv ≫ f.app _ ≫
      X.presheaf.map (eqToHom (f.preimage_image_eq U.unop).symm).op = 𝟙 _ := by
      rw [Scheme.Hom.appIso_inv_app_assoc, ← Functor.map_comp, ← X.presheaf.map_id]; rfl

Goal state after:
case refine_2
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
U : X.Opensᵒᵖ
x : ↑(X.ringCatSheaf.obj.obj U)
this :
  (Hom.appIso f (Opposite.unop U)).inv ≫ Scheme.Hom.app f (f ''ᵁ Opposite.unop U) ≫ X.presheaf.map (eqToHom ⋯).op =
    𝟙 Γ(X, Opposite.unop U)
⊢ (RingCat.Hom.hom
        (({
                  hom :=
                    Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
                      (forget₂ CommRingCat RingCat) }.hom ≫
              (Hom.opensFunctor f).op.whiskerLeft (Hom.toRingCatSheafHom f).hom ≫
                Functor.whiskerRight (NatTrans.op ⋯.adjunction.unit) X.ringCatSheaf.obj).app
          U))
      x =
    (RingCat.Hom.hom ((𝟙 X.ringCatSheaf.obj).app U)) x
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_deg : f ∈ 𝒜 m
q : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
i : ℕ
⊢ (proj 𝒜 i) a ^ m ∈ 𝒜 (m • i)

Tactic:
mem_tac

Goal state after:
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_deg : f ∈ 𝒜 m
q : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (i * m)

Tactic:
mem_tac

Goal state after:
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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
i : ℕ
⊢ (proj 𝒜 i) a ^ m ∈ 𝒜 (m • i)

Tactic:
mem_tac

Goal state after:
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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (i * m)

Tactic:
mem_tac

Goal state after:
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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ f ^ n ∈ 𝒜 (n * m)

Tactic:
mem_tac

Goal state after:
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
⊢ (proj 𝒜 n) a ^ m ∈ 𝒜 (m • n)

Tactic:
mem_tac

Goal state after:
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
⊢ f ^ n ∈ 𝒜 (n * m)

Tactic:
mem_tac

Goal state after:
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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
⊢ f ^ n ∈ 𝒜 (n * m)

Tactic:
mem_tac

Goal state after:
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 b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ f ^ i ∈ 𝒜 (i * m)

Tactic:
mem_tac

Goal state after:
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 b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ (proj 𝒜 i) b ^ m ∈ 𝒜 (m • i)

Tactic:
mem_tac

Goal state after:
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 b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
⊢ (proj 𝒜 i) a ^ m ∈ 𝒜 (m • i)

Tactic:
mem_tac

Goal state after:
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 b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
⊢ f ^ i ∈ 𝒜 (i * m)

Tactic:
mem_tac

Goal state after:
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 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ (awayMapAux 𝒜 ⋯) (mk { deg := n, num := a, den := ⟨f ^ i, hi⟩, den_mem := ⋯ }) =
    Localization.mk (↑a * g ^ i) ⟨x ^ i, ⋯⟩

Tactic:
by
  have : algebraMap A (Localization.Away x) f *
    (Localization.mk g ⟨f * g, (Submonoid.mem_powers_iff _ _).mpr ⟨1, by simp [hx]⟩⟩) = 1 := by
    rw [← Algebra.smul_def, Localization.smul_mk]
    exact Localization.mk_self ⟨f*g, _⟩
  simp only [awayMapAux, RingHom.coe_comp, Function.comp_apply, algebraMap_apply, val_mk]
  rw [Localization.awayLift_mk (hv := this), ← Algebra.smul_def,
    Localization.mk_pow, Localization.smul_mk]
  subst hx
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case refine_1.a
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 b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ (proj 𝒜 i) a ^ j ∈ 𝒜 ?refine_1.i

Tactic:
mem_tac

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case refine_1.a
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 b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ (proj 𝒜 i) b ^ (m - j) ∈ 𝒜 ?refine_1.j

Tactic:
mem_tac

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

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  ((Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))).inv ≫ Scheme.Hom.app (basicOpenToSpec 𝒜 f) ⊤) ≫
      (basicOpen 𝒜 f).topIso.hom =
    awayToSection 𝒜 f
⊢ IsIso (awayToSection 𝒜 f)

Tactic:
rw [← this, ← basicOpenIsoSpec_hom 𝒜 f f_deg hm]

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  ((Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))).inv ≫ Scheme.Hom.app (basicOpenToSpec 𝒜 f) ⊤) ≫
      (basicOpen 𝒜 f).topIso.hom =
    awayToSection 𝒜 f
⊢ IsIso
    (((Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))).inv ≫ Scheme.Hom.app (basicOpenIsoSpec 𝒜 f f_deg hm).hom ⊤) ≫
      (basicOpen 𝒜 f).topIso.hom)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case refine_2.a
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 b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
⊢ (proj 𝒜 i) a ^ (j - m) ∈ 𝒜 ((j - m) • i)

Tactic:
mem_tac

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case refine_2.a
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 b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
⊢ (proj 𝒜 i) b ^ (m + m - j) ∈ 𝒜 ((m + m - j) • i)

Tactic:
mem_tac

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

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
⊢ Localization.Away t →+* Localization.Away x

Tactic:
refine IsLocalization.map (M := .powers t) (T := .powers x) _ f ?_

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
⊢ Submonoid.powers t ≤ Submonoid.comap f (Submonoid.powers x)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case pos
ι : 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 𝒜
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)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
ai : ι' → ℕ
H : ∑ i, ai i • dv i = n
⊢ mk { deg := n, num := ((decompose 𝒜) (∏ i, v i ^ ai i)) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ } ∈
    {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}

Tactic:
refine ⟨j, ai, H.trans ?_, ?_⟩

Goal state after:
case pos.refine_1
ι : 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 𝒜
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)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
ai : ι' → ℕ
H : ∑ i, ai i • dv i = n
⊢ n = j • d

case pos.refine_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 𝒜
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)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
ai : ι' → ℕ
H : ∑ i, ai i • dv i = n
⊢ Away.mk 𝒜 hf j (∏ i, v i ^ ai i) ⋯ =
    mk { deg := n, num := ((decompose 𝒜) (∏ i, v i ^ ai i)) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ }
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
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
⊢ (proj 𝒜 (i - n)) x ^ m ∈ 𝒜 ?m.177

Tactic:
mem_tac

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case refine_2.refine_1
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
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
⊢ f ^ n ∈ 𝒜 ?m.422

Tactic:
mem_tac

Goal state after:
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)
⊢ SheafOfModules.Presentation (M.restrict (Opens.ι ((fun j ↦ ↑j.snd) i)))

Tactic:
let u := X.homOfLE (U := i.2) (V := W i.1) (by simp [heq, le_sSup])
    have : PreservesColimitsOfSize.{u, u} (restrictFunctor u) := inferInstance
    let F := (overEquiv (W i.1)).functor ⋙ restrictFunctor u
    let iso : SheafOfModules.overFunctor X.ringCatSheaf _ ⋙ F ≅ restrictFunctor
      (Scheme.Opens.ι i.2.1) := (Functor.associator _ _ _).symm ≪≫
        Functor.isoWhiskerRight (Scheme.Modules.overFunctorEquiv _) _ ≪≫
        (restrictFunctorComp _ _).symm ≪≫ (restrictFunctorCongr (by simp [u]))
    exact SheafOfModules.Presentation.ofIsIso.{u, u, u} (iso.app M).hom <|
      (pres i.1).map F (Scheme.Modules.restrictUnitIso _).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case refine_2.refine_2
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
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
⊢ f ^ (i - n) ∈ 𝒜 ?m.461

Tactic:
mem_tac

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

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : mR ≤ M
fSₘ : LocalSubring K := ofPrime S M
| maximalIdeal ↥fSₘ.toSubring

Tactic:
rw [← IsLocalization.AtPrime.map_eq_maximalIdeal M]

Goal state after:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬mR = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : mR ≤ M
fSₘ : LocalSubring K := ofPrime S M
| Ideal.map (algebraMap ↥S ↥fSₘ.toSubring) M
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
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (ConcreteCategory.hom (toSpec 𝒜 f).base) x =
    PrimeSpectrum.comap (mapId 𝒜 ⋯) (closedPoint (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))

Tactic:
change PrimeSpectrum.comap (awayToΓ 𝒜 f ≫ (Proj| pbo f).presheaf.Γgerm x).hom
        (IsLocalRing.closedPoint ((Proj| pbo f).presheaf.stalk x)) = _

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
⊢ PrimeSpectrum.comap (CommRingCat.Hom.hom (awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x))
      (closedPoint ↑((Proj.restrict ⋯).presheaf.stalk x)) =
    PrimeSpectrum.comap (mapId 𝒜 ⋯) (closedPoint (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case mp
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ (Sieve.overEquiv X) R ∈ (grothendieckTopology P) X.left → R ∈ (overPretopology P S).toGrothendieck X

Tactic:
intro hR
    obtain ⟨𝒰, hle⟩ := exists_cover_of_mem_grothendieckTopology hR
    rw [mem_grothendieckTopology_iff] at hR
    let (i : 𝒰.I₀) : (𝒰.X i).Over S := { hom := 𝒰.f i ≫ X.hom }
    let : 𝒰.Over S :=
      { over := inferInstance
        isOver_map := fun i ↦ ⟨rfl⟩ }
    use 𝒰.toPresieveOver, ⟨𝒰, inferInstance, rfl⟩
    rwa [Cover.toPresieveOver_le_arrows_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X : C
data : F.PreOneHypercoverDenseData X
i₁ i₂ : data.I₀
W₀ : C₀
p₁ : W₀ ⟶ data.X i₁
p₂ : W₀ ⟶ data.X i₂
⊢ ∀ {Y Z : C₀} {f : Y ⟶ W₀},
    (∃ j h, f ≫ p₁ = h ≫ data.p₁ j ∧ f ≫ p₂ = h ≫ data.p₂ j) →
      ∀ (g : Z ⟶ Y), ∃ j h, (g ≫ f) ≫ p₁ = h ≫ data.p₁ j ∧ (g ≫ f) ≫ p₂ = h ≫ data.p₂ j

Tactic:
by
    rintro Z Z' g ⟨j, h, fac₁, fac₂⟩ φ
    exact ⟨j, φ ≫ h, by simpa using φ ≫= fac₁, by simpa using φ ≫= fac₂⟩

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

Goal state before:
pp: ⊢ zariskiTopology ≤ etaleTopology

Tactic:
apply grothendieckTopology_monotone
  intro X Y f hf
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝ : P.IsStableUnderComposition
K : Precoverage C
H : K ≤ P.precoverage
X : P.Over ⊤ S
R : Presieve ((Over.forget P ⊤ S).obj X)
hR : R ∈ (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj X)
⊢ ∃ T, Presieve.map (Over.forget P ⊤ S) T = R

Tactic:
rw [Precoverage.mem_iff_exists_zeroHypercover] at hR

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝ : P.IsStableUnderComposition
K : Precoverage C
H : K ≤ P.precoverage
X : P.Over ⊤ S
R : Presieve ((Over.forget P ⊤ S).obj X)
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ ∃ T, Presieve.map (Over.forget P ⊤ S) T = R
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this : Mono f
A✝ : C
g : A✝ ⟶ X
inst✝ : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk g
c' : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X) :=
  { pt := A✝, ι := { app := fun j ↦ Subobject.ofMkLEMk (F.obj j).obj.hom g ⋯, naturality := ⋯ } }
j : J
⊢ c'.ι.app j ≫ g = (F.obj j).obj.hom

Tactic:
Subobject.ofMkLEMk_comp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this : Mono f
A✝ : C
g : A✝ ⟶ X
inst✝ : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk g
c' : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X) :=
  { pt := A✝, ι := { app := fun j ↦ Subobject.ofMkLEMk (F.obj j).obj.hom g ⋯, naturality := ⋯ } }
j : J
⊢ (F.obj j).obj.hom = (F.obj j).obj.hom
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
x✝ : Discrete c.ι
i : c.ι
⊢ (Discrete.functor fun i ↦ A (c.π i)).obj { as := i } ⟶ (Discrete.functor fun i ↦ B (c.π i)).obj { as := i }

Tactic:
by exact g (c.π i)

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case inl
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (F.map (homOfLE hij').op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val)) =
    (ConcreteCategory.hom (F.map (homOfLE hij').op)) e.val
⊢ (ConcreteCategory.hom (F.map (homOfLE hij✝).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val),
        ⋯⟩

Tactic:
rw [e.map_limit i hi, ← comp_apply, ← map_comp, ← op_comp, homOfLE_comp] at this

Goal state after:
case inl
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val,
        ⋯⟩
⊢ (ConcreteCategory.hom (F.map (homOfLE hij✝).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val),
        ⋯⟩
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingProperty (F.map (homOfLE ⋯)) p
f✝ : F.obj ⊥ ⟶ X
g✝ : ((Functor.const J).obj c.pt).obj ⊥ ⟶ Y
sq : CommSq f✝ (c.ι.app ⊥) p g✝
j : J
hj : ¬IsMax j
x✝¹ : F.obj j ⟶ X
x✝ : CommSq x✝¹ (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g✝)
⊢ x✝.HasLift

Tactic:
by have := hF j hj; infer_instance

Goal state after: