mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
⊢ X.basicOpen (f r) ≤ fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r

Tactic:
intro x hx
    let I : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀ := ⟨n, r, hn, hr⟩
    obtain ⟨x, rfl⟩ : x ∈ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f I).opensRange := by
      simpa [openCoverOfMapIrrelevantEqTop] using hx
    rw [← SetLike.mem_coe] -- TODO : mem version of TopologicalSpace.Opens.map_coe
    simp only [TopologicalSpace.Opens.map_coe, Set.mem_preimage,
      ← Scheme.Hom.comp_apply, fromOfGlobalSections]
    simp

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, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
⊢ (X.basicOpen (f r)).ι ≫
      Scheme.Cover.glueMorphisms (openCoverOfMapIrrelevantEqTop 𝒜 f hf)
        (fun ri ↦ toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫ (basicOpen 𝒜 ri.snd.fst).ι) ⋯ =
    toBasicOpenOfGlobalSections 𝒜 f ⋯ hn hr ≫ (basicOpen 𝒜 r).ι

Tactic:
exact (openCoverOfMapIrrelevantEqTop 𝒜 f hf).ι_glueMorphisms _ _ ⟨_, _, hn, hr⟩

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, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
⊢ fromOfGlobalSections 𝒜 f hf ∣_ basicOpen 𝒜 r = (X.isoOfEq ⋯).hom ≫ toBasicOpenOfGlobalSections 𝒜 f ⋯ hn hr

Tactic:
by
  rw [← Iso.inv_comp_eq, ← cancel_mono (basicOpen 𝒜 r).ι]
  simp only [Scheme.isoOfEq_inv, Category.assoc, morphismRestrict_ι, Scheme.homOfLE_ι_assoc,
    fromOfGlobalSections]
  exact (openCoverOfMapIrrelevantEqTop 𝒜 f hf).ι_glueMorphisms _ _ ⟨_, _, hn, hr⟩

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

Goal state before:
pp: case e_a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ Spec.map
      (CommRingCat.ofHom
        (((IsLocalization.map (Localization.Away (f x.snd.fst)) f ⋯).comp
              (algebraMap (Away 𝒜 x.snd.fst) (Localization.Away x.snd.fst))).comp
          (algebraMap (↥(𝒜 0)) (HomogeneousLocalization 𝒜 (Submonoid.powers x.snd.fst))))) =
    Spec.map
      (CommRingCat.ofHom
        ((algebraMap (↑Γ(X, ⊤)) (Localization.Away (f x.snd.fst))).comp (f.comp (algebraMap (↥(𝒜 0)) A))))

Tactic:
congr 2

Goal state after:
case e_a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ ((IsLocalization.map (Localization.Away (f x.snd.fst)) f ⋯).comp
          (algebraMap (Away 𝒜 x.snd.fst) (Localization.Away x.snd.fst))).comp
      (algebraMap (↥(𝒜 0)) (HomogeneousLocalization 𝒜 (Submonoid.powers x.snd.fst))) =
    (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f x.snd.fst))).comp (f.comp (algebraMap (↥(𝒜 0)) A))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_2
X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
I : Type u
W : I → TopologicalSpace.Opens ↥X
cov : iSup 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
⊢ ⨆ j, ↑⟨i, j⟩.snd = sSup (κ i)

Tactic:
sSup_eq_iSup'

Goal state after:
case refine_2
X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
I : Type u
W : I → TopologicalSpace.Opens ↥X
cov : iSup 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
⊢ ⨆ j, ↑⟨i, j⟩.snd = ⨆ a, ↑a
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
⊢ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) ≤ Ideal.map (algebraMap ↥S ↥fSₘ.toSubring) M

Tactic:
refine .trans ?_ (Ideal.map_mono h_incl)

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 (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) ≤ Ideal.map (algebraMap ↥S ↥fSₘ.toSubring) mR
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: 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
i : ι
n : ℕ
t' : ↑Γ(M, basicOpen (g i))
ht' : (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t' = g i ^ n • f ^ n • s' i
⊢ ∃ n t, f ^ n • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t

Tactic:
obtain ⟨ψ, hψ⟩ := IsUnit.exists_right_inv (hug i n)

Goal state after:
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
i : ι
n : ℕ
t' : ↑Γ(M, basicOpen (g i))
ht' : (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t' = g i ^ n • f ^ n • s' i
ψ : Module.End ↑R ↑Γ(M, basicOpen (g i))
hψ : (algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ n) * ψ = 1
⊢ ∃ n t, f ^ n • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t
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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ∃ V,
    ∃ (_ : ↑x ∈ V),
      ∃ i,
        (isFractionPrelocal 𝒜).pred fun x ↦
          (fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) (HomogeneousLocalization.mk s)) (i x)

Tactic:
obtain ⟨n, hn : f ^ n = s.den.1⟩ := s.den_mem

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = ↑s.den
⊢ ∃ V,
    ∃ (_ : ↑x ∈ V),
      ∃ i,
        (isFractionPrelocal 𝒜).pred fun x ↦
          (fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) (HomogeneousLocalization.mk s)) (i x)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case exists_of_eq
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e✝ :
  (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk y) =
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk z)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x).asHomogeneousIdeal
e : c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)
⊢ (algebraMap A (Localization (Submonoid.powers f))) (f ^ i * (↑z.den * (c ^ m * ↑y.num))) =
    (algebraMap A (Localization (Submonoid.powers f))) (f ^ i * (↑y.den * (c ^ m * ↑z.num)))

Tactic:
congr 2

Goal state after:
case exists_of_eq.e_6.e_a
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e✝ :
  (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk y) =
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk z)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x).asHomogeneousIdeal
e : c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)
⊢ ↑z.den * (c ^ m * ↑y.num) = ↑y.den * (c ^ m * ↑z.num)
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✝³ : IsDenseSubsite J₀ J F
inst✝² : HasPullbacks C
inst✝¹ : F.Full
inst✝ : F.Faithful
S : C
ι : C → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun i ↦ F.obj (U S i)) (f S) ∈ J S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
T : C
Z : C₀
q : Z ⟶ W₀
r : T ⟶ F.obj Z
Y : C
k : ι (pullback (f S i) (f S j))
s : F.obj Z ⟶ F.obj (U (pullback (f S i) (f S j)) k)
fac : s ≫ f (pullback (f S i) (f S j)) k = F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp
fac₁ : s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j) = F.map q ≫ F.map p₁
fac₂ : s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j) = F.map q ≫ F.map p₂
⊢ F.map (q ≫ p₂) =
    F.map
      (F.preimage s ≫
        { I₀ := ι S, X := U S, f := f S, I₁ := fun i j ↦ ι (pullback (f S i) (f S j)),
              Y := fun i j ↦ U (pullback (f S i) (f S j)),
              p₁ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
              p₂ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)), w := ⋯ }.p₂
          k)

Tactic:
simp [fac₂]

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

Goal state before:
pp: case refine_1
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : IsLocalizing (modulesSpecToSheaf.obj M)
hf : ∀ (f : ↑R), IsLocalizedModule.Away f (φ f)
⊢ Aux M ⊤

Tactic:
refine ⟨fun f hle s ↦ ?_, fun f hle s hs ↦ ?_⟩

Goal state after:
case refine_1.refine_1
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : IsLocalizing (modulesSpecToSheaf.obj M)
hf : ∀ (f : ↑R), IsLocalizedModule.Away f (φ f)
f : ↑R
hle : basicOpen f ≤ ⊤
s : ↑Γ(M, basicOpen f)
⊢ ∃ n t, (ConcreteCategory.hom (M.presheaf.map (homOfLE hle).op)) t = f ^ n • s

case refine_1.refine_2
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : IsLocalizing (modulesSpecToSheaf.obj M)
hf : ∀ (f : ↑R), IsLocalizedModule.Away f (φ f)
f : ↑R
hle : basicOpen f ≤ ⊤
s : ↑Γ(M, ⊤)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hle).op)) s = 0
⊢ ∃ n, f ^ n • s = 0
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case refine_1
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✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
this : F.IsCoverDense J
S : Sieve W :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
hS : S ∈ J W
hT : T ∈ J W
U V : C
a : U ⟶ V
b : V ⟶ W
hb : S.arrows b
str : Presieve.FunctorPushforwardStructure F
  (F.imageSieve ((Nonempty.some ⋯).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some ⋯).map ≫ p₂)).arrows
  ((Presieve.bind.bindStruct hb).g ≫ (Nonempty.some ⋯).lift) :=
  Presieve.getFunctorPushforwardStructure ⋯
W₀ : C₀
c : W₀ ⟶ (Presieve.getFunctorPushforwardStructure ⋯).preobj
d : U ⟶ F.obj W₀
fac : a ≫ (Presieve.getFunctorPushforwardStructure ⋯).lift = d ≫ F.map c
j : data.I₁ i₁ i₂
e : W₀ ⟶ data.Y j
h₁ : c ≫ Exists.choose ⋯ = e ≫ data.p₁ j
h₂ : c ≫ Exists.choose ⋯ = e ≫ data.p₂ j
⊢ a ≫ b ≫ p₁ = d ≫ F.map e ≫ F.map (data.p₁ j)

Tactic:
← F.map_comp,

Goal state after:
case refine_1
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✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
this : F.IsCoverDense J
S : Sieve W :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
hS : S ∈ J W
hT : T ∈ J W
U V : C
a : U ⟶ V
b : V ⟶ W
hb : S.arrows b
str : Presieve.FunctorPushforwardStructure F
  (F.imageSieve ((Nonempty.some ⋯).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some ⋯).map ≫ p₂)).arrows
  ((Presieve.bind.bindStruct hb).g ≫ (Nonempty.some ⋯).lift) :=
  Presieve.getFunctorPushforwardStructure ⋯
W₀ : C₀
c : W₀ ⟶ (Presieve.getFunctorPushforwardStructure ⋯).preobj
d : U ⟶ F.obj W₀
fac : a ≫ (Presieve.getFunctorPushforwardStructure ⋯).lift = d ≫ F.map c
j : data.I₁ i₁ i₂
e : W₀ ⟶ data.Y j
h₁ : c ≫ Exists.choose ⋯ = e ≫ data.p₁ j
h₂ : c ≫ Exists.choose ⋯ = e ≫ data.p₂ j
⊢ a ≫ b ≫ p₁ = d ≫ F.map (e ≫ data.p₁ j)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case refine_2
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✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
this : F.IsCoverDense J
S : Sieve W :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
hS : S ∈ J W
hT : T ∈ J W
U V : C
a : U ⟶ V
b : V ⟶ W
hb : S.arrows b
str : Presieve.FunctorPushforwardStructure F
  (F.imageSieve ((Nonempty.some ⋯).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some ⋯).map ≫ p₂)).arrows
  ((Presieve.bind.bindStruct hb).g ≫ (Nonempty.some ⋯).lift) :=
  Presieve.getFunctorPushforwardStructure ⋯
W₀ : C₀
c : W₀ ⟶ (Presieve.getFunctorPushforwardStructure ⋯).preobj
d : U ⟶ F.obj W₀
fac : a ≫ (Presieve.getFunctorPushforwardStructure ⋯).lift = d ≫ F.map c
j : data.I₁ i₁ i₂
e : W₀ ⟶ data.Y j
h₁ : c ≫ Exists.choose ⋯ = e ≫ data.p₁ j
h₂ : c ≫ Exists.choose ⋯ = e ≫ data.p₂ j
⊢ a ≫ b ≫ p₂ = d ≫ F.map e ≫ F.map (data.p₂ j)

Tactic:
← F.map_comp,

Goal state after:
case refine_2
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✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
this : F.IsCoverDense J
S : Sieve W :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
hS : S ∈ J W
hT : T ∈ J W
U V : C
a : U ⟶ V
b : V ⟶ W
hb : S.arrows b
str : Presieve.FunctorPushforwardStructure F
  (F.imageSieve ((Nonempty.some ⋯).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some ⋯).map ≫ p₂)).arrows
  ((Presieve.bind.bindStruct hb).g ≫ (Nonempty.some ⋯).lift) :=
  Presieve.getFunctorPushforwardStructure ⋯
W₀ : C₀
c : W₀ ⟶ (Presieve.getFunctorPushforwardStructure ⋯).preobj
d : U ⟶ F.obj W₀
fac : a ≫ (Presieve.getFunctorPushforwardStructure ⋯).lift = d ≫ F.map c
j : data.I₁ i₁ i₂
e : W₀ ⟶ data.Y j
h₁ : c ≫ Exists.choose ⋯ = e ≫ data.p₁ j
h₂ : c ≫ Exists.choose ⋯ = e ≫ data.p₂ j
⊢ a ≫ b ≫ p₂ = d ≫ F.map (e ≫ data.p₂ j)
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
inst✝ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha : (↑⟨Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) ↑S), ⋯⟩).arrows a
ha₁ : (↑S).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
⊢ s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁, hf := ha₁ } =
    s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂, hf := ha₂ }

Tactic:
congr 2

Goal state after:
case e_6
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
inst✝ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha : (↑⟨Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) ↑S), ⋯⟩).arrows a
ha₁ : (↑S).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
⊢ F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁ = F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂
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 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := IsLocalization.Away.lift (Away.isLocalizationElem ⋯ ⋯) hunit
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
sx : Away 𝒜 (x i₀)
a : ℕ
ai : ι → ℕ
hai✝ : ∑ i, ai i • d i = a • d i₀
hai : ∑ x, ai x * d x = a * d i₀
H : (∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1)) ∈ 𝒜 ((a * d i₀) • d j)
⊢ (valuation O K) (φ ((Away.isLocalizationElem ⋯ ⋯ ^ ∏ k ∈ Finset.univ.erase i₀, d k) ^ (d i₀ * a * d j))) =
    (valuation O K) (φ ((Away.isLocalizationElem ⋯ ⋯ ^ a) ^ (d j * ∏ k, d k)))

Tactic:
congr 2

Goal state after:
case e_6.e_6
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := ⋯
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := ⋯
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := ⋯
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
sx : Away 𝒜 (x i₀)
a : ℕ
ai : ι → ℕ
hai✝ : ∑ i, ai i • d i = a • d i₀
hai : ∑ x, ai x * d x = a * d i₀
H : (∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1)) ∈ 𝒜 ((a * d i₀) • d j)
⊢ (Away.isLocalizationElem ⋯ ⋯ ^ ∏ k ∈ Finset.univ.erase i₀, d k) ^ (d i₀ * a * d j) =
    (Away.isLocalizationElem ⋯ ⋯ ^ a) ^ (d j * ∏ k, d k)