mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ {
        hom :=
          Functor.whiskerRight { app := fun U ↦ (Hom.appIso (𝟙 X) (Opposite.unop U)).inv, naturality := ⋯ }
            (forget₂ CommRingCat RingCat) } ≫
      (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯).hom RingCat
            (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥X)).app
        X.ringCatSheaf =
    𝟙 X.ringCatSheaf

Tactic:
ext : 3

Goal state after:
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
x✝ : (TopologicalSpace.Opens ↥X)ᵒᵖ
⊢ ({
              hom :=
                Functor.whiskerRight { app := fun U ↦ (Hom.appIso (𝟙 X) (Opposite.unop U)).inv, naturality := ⋯ }
                  (forget₂ CommRingCat RingCat) } ≫
            (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯).hom RingCat
                  (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥X)).app
              X.ringCatSheaf).hom.app
      x✝ =
    (𝟙 X.ringCatSheaf).hom.app x✝
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
⊢ {
        hom :=
          Functor.whiskerRight { app := fun U ↦ (Hom.appIso (f ≫ g) (Opposite.unop U)).inv, naturality := ⋯ }
            (forget₂ CommRingCat RingCat) } ≫
      (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯).hom RingCat
            (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Z)).app
        Z.ringCatSheaf =
    {
        hom :=
          Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
            (forget₂ CommRingCat RingCat) } ≫
      ((Hom.opensFunctor f).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥X)
            (Opens.grothendieckTopology ↥Y)).map
        {
          hom :=
            Functor.whiskerRight { app := fun U ↦ (Hom.appIso g (Opposite.unop U)).inv, naturality := ⋯ }
              (forget₂ CommRingCat RingCat) }

Tactic:
ext : 3

Goal state after:
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
x✝ : (TopologicalSpace.Opens ↥X)ᵒᵖ
⊢ ({
              hom :=
                Functor.whiskerRight { app := fun U ↦ (Hom.appIso (f ≫ g) (Opposite.unop U)).inv, naturality := ⋯ }
                  (forget₂ CommRingCat RingCat) } ≫
            (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯).hom RingCat
                  (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Z)).app
              Z.ringCatSheaf).hom.app
      x✝ =
    ({
              hom :=
                Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
                  (forget₂ CommRingCat RingCat) } ≫
            ((Hom.opensFunctor f).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥X)
                  (Opens.grothendieckTopology ↥Y)).map
              {
                hom :=
                  Functor.whiskerRight { app := fun U ↦ (Hom.appIso g (Opposite.unop U)).inv, naturality := ⋯ }
                    (forget₂ CommRingCat RingCat) }).hom.app
      x✝
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 g : X ⟶ Y
hf : f = g
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ {
        hom :=
          Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
            (forget₂ CommRingCat RingCat) } ≫
      (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯).hom RingCat
            (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Y)).app
        Y.ringCatSheaf =
    {
      hom :=
        Functor.whiskerRight { app := fun U ↦ (Hom.appIso g (Opposite.unop U)).inv, naturality := ⋯ }
          (forget₂ CommRingCat RingCat) }

Tactic:
ext : 3

Goal state after:
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 g : X ⟶ Y
hf : f = g
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
x✝ : (TopologicalSpace.Opens ↥X)ᵒᵖ
⊢ ({
              hom :=
                Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
                  (forget₂ CommRingCat RingCat) } ≫
            (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯).hom RingCat
                  (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Y)).app
              Y.ringCatSheaf).hom.app
      x✝ =
    {
            hom :=
              Functor.whiskerRight { app := fun U ↦ (Hom.appIso g (Opposite.unop U)).inv, naturality := ⋯ }
                (forget₂ CommRingCat RingCat) }.hom.app
      x✝
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 𝒜
x : Submonoid A
f : NumDenSameDeg 𝒜 x
h : f.den = 0
⊢ mk f = 0

Tactic:
have := subsingleton 𝒜 (h ▸ f.den_mem)
  exact Subsingleton.elim _ _

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 𝒜
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
f : 𝒜 →+*ᵍ ℬ
I : Ideal A
inst✝¹ : I.IsPrime
J : Ideal B
inst✝ : J.IsPrime
hIJ : I = Ideal.comap f J
x : AtPrime 𝒜 I
hx : IsUnit ((localRingHom f I J hIJ) x)
⊢ IsUnit x

Tactic:
rw [← isUnit_iff_isUnit_val] at hx ⊢

Goal state after:
ι : 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
f : 𝒜 →+*ᵍ ℬ
I : Ideal A
inst✝¹ : I.IsPrime
J : Ideal B
inst✝ : J.IsPrime
hIJ : I = Ideal.comap f J
x : AtPrime 𝒜 I
hx : IsUnit (val ((localRingHom f I J hIJ) x))
⊢ IsUnit (val x)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case neg.mem
ι : 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
a : A
ha' : a ∈ ↑(Submonoid.closure (Set.range v))
⊢ mk { deg := n, num := ((decompose 𝒜) a) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ } ∈
    Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}

Tactic:
| mem a ha' =>

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

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f : (↑R)ᵒᵖ
⊢ ((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
          (modulesSpecToSheaf.obj (tilde ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)))).obj).obj
      f ⟶
    ((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).obj f

Tactic:
refine (ModuleCat.ofHom (IsLocalizedModule.lift (.powers (M := R) f.unop)
          (tilde.toOpen _ (PrimeSpectrum.basicOpen f.unop)).hom
          ((modulesSpecToSheaf.obj M).obj.map (homOfLE le_top).op).hom ?_):)

Goal state after:
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f : (↑R)ᵒᵖ
⊢ ∀ (x : ↥(Submonoid.powers (unop f))),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑((modulesSpecToSheaf.obj M).obj.obj (op ((inducedFunctor PrimeSpectrum.basicOpen).obj (unop f))))))
        ↑x)
Module: Mathlib.RingTheory.LocalRing.LocalSubring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
⊢ Localization.AtPrime P ≃ₐ[↥A] ↥(ofPrime A P).toSubring

Tactic:
by
  refine AlgEquiv.ofInjective (IsLocalization.liftAlgHom (M := P.primeCompl)
    (S := Localization.AtPrime P) (f := Algebra.ofId A K) _) ?_
  intro x y e
  obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq P.primeCompl x
  obtain ⟨y, t, rfl⟩ := IsLocalization.exists_mk'_eq P.primeCompl y
  have H : ∀ x : P.primeCompl, x.1 ≠ 0 := by rintro ⟨x, hx⟩ rfl; aesop
  have : x.1 = y.1 * t.1.1⁻¹ * s.1.1 := by
    simpa [IsLocalization.lift_mk', Algebra.ofId_apply, H,
      Algebra.algebraMap_ofSubsemiring_apply, IsUnit.coe_liftRight] using congr($e * s.1.1)
  rw [IsLocalization.mk'_eq_iff_eq]
  congr 1
  ext
  simp [field, H t, this, mul_comm]

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

Goal state before:
pp: case refine_1
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)
s : Finset ι' := {x | 0 < dv x}
⊢ ∀ (y : ι'), v y ∈ ↑(Algebra.adjoin (↥(𝒜 0)) (Set.range (v ∘ Subtype.val)))

Tactic:
intro i

Goal state after:
case refine_1
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)
s : Finset ι' := {x | 0 < dv x}
i : ι'
⊢ v i ∈ ↑(Algebra.adjoin (↥(𝒜 0)) (Set.range (v ∘ Subtype.val)))
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
x : ↑↑(Proj.restrict ⋯).toPresheafedSpace
⊢ ∀ (i : ℕ),
    ∀ x_1 ∈ 𝒜 i,
      x_1 ∈ (↑(FromSpec.toFun f_deg hm ((ConcreteCategory.hom (toSpec 𝒜 f)) x))).asHomogeneousIdeal ↔
        x_1 ∈ (↑x).asHomogeneousIdeal

Tactic:
intro i

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
x : ↑↑(Proj.restrict ⋯).toPresheafedSpace
i : ℕ
⊢ ∀ x_1 ∈ 𝒜 i,
    x_1 ∈ (↑(FromSpec.toFun f_deg hm ((ConcreteCategory.hom (toSpec 𝒜 f)) x))).asHomogeneousIdeal ↔
      x_1 ∈ (↑x).asHomogeneousIdeal
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: case inr
K : Type u_3
inst✝¹ : Field K
x : K
R : LocalSubring K
hxR : x ∉ R.toSubring
inst✝ : IsIntegrallyClosedIn (↥R.toSubring) K
hx0 : x ≠ 0
this✝ : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := ⟨x⁻¹, ⋯⟩
this : Ideal.map (algebraMap ↥R.toSubring ↥B) (maximalIdeal ↥R.toSubring) + Ideal.span {xinv} ≠ ⊤
V : ValuationSubring K
hV :
  B.toSubring ≤ V.toSubring ∧
    ⇑B.toSubring.subtype '' ↑(Ideal.map (algebraMap ↥R.toSubring ↥B) (maximalIdeal ↥R.toSubring) + Ideal.span {xinv}) ⊆
      ↑V.nonunits
⊢ ∃ V, R ≤ V.toLocalSubring ∧ x ∉ V

Tactic:
refine ⟨V, ⟨fun r hr ↦ hV.1 (B.algebraMap_mem ⟨r, hr⟩),
    ((local_hom_TFAE _).out 3 0).mp fun r hr ↦ ?_⟩, (V.inv_mem_nonunits_iff.mp <|
      hV.2 ⟨_, le_add_self (α := Ideal B) (Ideal.subset_span rfl), rfl⟩).resolve_left hx0⟩

Goal state after:
case inr
K : Type u_3
inst✝¹ : Field K
x : K
R : LocalSubring K
hxR : x ∉ R.toSubring
inst✝ : IsIntegrallyClosedIn (↥R.toSubring) K
hx0 : x ≠ 0
this✝ : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
xinv : ↥B.toSubring := ⟨x⁻¹, ⋯⟩
this : Ideal.map (algebraMap ↥R.toSubring ↥B) (maximalIdeal ↥R.toSubring) + Ideal.span {xinv} ≠ ⊤
V : ValuationSubring K
hV :
  B.toSubring ≤ V.toSubring ∧
    ⇑B.toSubring.subtype '' ↑(Ideal.map (algebraMap ↥R.toSubring ↥B) (maximalIdeal ↥R.toSubring) + Ideal.span {xinv}) ⊆
      ↑V.nonunits
r : ↥R.toSubring
hr : r ∈ maximalIdeal ↥R.toSubring
⊢ r ∈ Ideal.comap (Subring.inclusion ⋯) (maximalIdeal ↥V.toLocalSubring.toSubring)
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
⊢ IsIso (toSpec 𝒜 f)

Tactic:
by
  have : IsIso (toSpec 𝒜 f).base := toSpec_base_isIso 𝒜 f_deg hm
  have _ (x) : IsIso ((toSpec 𝒜 f).stalkMap x) := by
    rw [stalkMap_toSpec 𝒜 f x f_deg hm]; infer_instance
  have : LocallyRingedSpace.IsOpenImmersion (toSpec 𝒜 f) :=
    LocallyRingedSpace.IsOpenImmersion.of_stalk_iso (toSpec 𝒜 f)
      (TopCat.homeoOfIso (asIso <| (toSpec 𝒜 f).base)).isOpenEmbedding
  exact LocallyRingedSpace.IsOpenImmersion.to_iso _

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

Goal state before:
pp: case h.refine_2
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
a : ToType ({ obj := M.presheaf, property := ⋯ }.obj.obj (op V))
ha : ∀ (i : ι), (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) a = f ^ K • t i
⊢ ∀ (i : ι),
    (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) a) =
      (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) (f ^ (N + K) • s)

Tactic:
intro i

Goal state after:
case h.refine_2
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
a : ToType ({ obj := M.presheaf, property := ⋯ }.obj.obj (op V))
ha : ∀ (i : ι), (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) a = f ^ K • t i
i : ι
⊢ (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) a) =
    (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) (f ^ (N + K) • s)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1.refine_1
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
⊢ Presheaf.IsCompatible { obj := M.presheaf, property := ⋯ }.obj (fun i ↦ basicOpen (g i)) fun i ↦ f ^ K • t i

Tactic:
intro i

Goal state after:
case refine_1.refine_1
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
i : ι
⊢ ∀ (j : ι),
    (ConcreteCategory.hom
          ({ obj := M.presheaf, property := ⋯ }.obj.map
            (((fun i ↦ basicOpen (g i)) i).infLELeft ((fun i ↦ basicOpen (g i)) j)).op))
        ((fun i ↦ f ^ K • t i) i) =
      (ConcreteCategory.hom
          ({ obj := M.presheaf, property := ⋯ }.obj.map
            (((fun i ↦ basicOpen (g i)) i).infLERight ((fun i ↦ basicOpen (g i)) j)).op))
        ((fun i ↦ f ^ K • t i) j)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
⊢ ∀ (i : ↥x), LocallyOfFiniteType ((basicOpen 𝒜 ↑i).ι ≫ toSpecZero 𝒜)

Tactic:
intro i

Goal state after:
σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
⊢ LocallyOfFiniteType ((basicOpen 𝒜 ↑i).ι ≫ toSpecZero 𝒜)
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ R ∈ (smallGrothendieckTopology P S) X ↔ ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows

Tactic:
by
  rw [smallGrothendieckTopology_eq_toGrothendieck_smallPretopology _ le_rfl]
  constructor
  · rintro ⟨T, ⟨𝒰, h, p, rfl⟩, hle⟩
    use 𝒰, h, p
  · rintro ⟨𝒰, h𝒰, p, hle⟩
    exact ⟨𝒰.toPresieveOverProp p, ⟨𝒰, h𝒰, p, rfl⟩, hle⟩

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
inst✝² : F.IsOneHypercoverDense J₀ J
inst✝¹ : F.IsLocallyFull J
inst✝ : F.IsLocallyFaithful J
h : ∀ {X₀ : C₀} {S₀ : Sieve X₀}, Sieve.functorPushforward F S₀ ∈ J.sieves (F.obj X₀) ↔ S₀ ∈ J₀.sieves X₀
X : C
⊢ Sieve.coverByImage F X ∈ J X

Tactic:
refine J.superset_covering ?_ (F.oneHypercoverDenseData J₀ J X).mem₀

Goal state after:
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
inst✝² : F.IsOneHypercoverDense J₀ J
inst✝¹ : F.IsLocallyFull J
inst✝ : F.IsLocallyFaithful J
h : ∀ {X₀ : C₀} {S₀ : Sieve X₀}, Sieve.functorPushforward F S₀ ∈ J.sieves (F.obj X₀) ↔ S₀ ∈ J₀.sieves X₀
X : C
⊢ (F.oneHypercoverDenseData J₀ J X).toPreOneHypercover.sieve₀ ≤ Sieve.coverByImage F X
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h.h
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
⊢ ∀ (i : ι),
    (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) ((f ^ ⨆ i, n i) • t) =
      (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) 0

Tactic:
intro i

Goal state after:
case h.h
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
i : ι
⊢ (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) ((f ^ ⨆ i, n i) • t) =
    (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) 0