mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent

Goal state before:
pp: X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝¹ : IsNoetherian X
inst✝ : IrreducibleSpace ↥X
this : CategoryTheory.IsIso (X.irreducibleComponentOpen Z).ι
⊢ CategoryTheory.IsIso (X.irreducibleComponentι Z hZ)

Tactic:
irreducibleComponentι,

Goal state after:
X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝¹ : IsNoetherian X
inst✝ : IrreducibleSpace ↥X
this : CategoryTheory.IsIso (X.irreducibleComponentOpen Z).ι
⊢ CategoryTheory.IsIso (X.irreducibleComponentIdeal Z hZ).subschemeι
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case e'_2.e'_7
R : Type u
S : Type (max u v)
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
p : Ideal R
inst✝¹⁶ : p.IsPrime
q : Ideal S
R' : Type u
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : Algebra R R'
inst✝¹³ : Etale R R'
P : Ideal R'
inst✝¹² : P.IsPrime
inst✝¹¹ : P.LiesOver p
e : R' ⊗[R] S
P' : Ideal (R' ⊗[R] S)
inst✝¹⁰ : P'.IsPrime
inst✝⁹ : P'.LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
heP' : e ∉ P'
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
R'' : Type u
inst✝⁸ : CommRing R''
inst✝⁷ : Algebra R' R''
inst✝⁶ : Algebra R R''
inst✝⁵ : IsScalarTower R R' R''
inst✝⁴ : Etale R' R''
Q : Ideal R''
inst✝³ : Q.IsPrime
inst✝² : Q.LiesOver P
n : ℕ
e' : Fin (n + 1 + 1) → R'' ⊗[R] S
he' : CompleteOrthogonalIdempotents e'
he'0 : e' 0 = (TensorProduct.map (ofId R' R'') (AlgHom.id R S)) e
Q' : Fin n → Ideal (R'' ⊗[R] S)
inst✝¹ : ∀ (i : Fin n), (Q' i).IsPrime
inst✝ : ∀ (i : Fin n), (Q' i).LiesOver Q
hPQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (ofId R' R'') ⋯)
hQ' : ∀ (i : Fin n), e' i.succ.castSucc ∉ Q' i
H' :
  ∀ (P'' : Ideal (R'' ⊗[R] S)),
    e' 0 ∈ P'' →
      P''.IsPrime → P''.LiesOver Q → e' (Fin.last (n + 1)) ∈ P'' ∧ ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Q' i
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.map (ofId R' R'') (AlgHom.id R S)
this✝¹ : Q.LiesOver p
hpQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p Q (ofId R R'') ⋯)
P'φ : ↑(Q.primesOver (R'' ⊗[R] S)) :=
  (Ideal.fiberIsoOfBijectiveResidueField hpQ).symm ((Ideal.fiberIsoOfBijectiveResidueField hpP) ⟨P', ⋯⟩)
this✝ : (↑P'φ).LiesOver P
this : (Ideal.comap φ.toRingHom ↑P'φ).LiesOver P
⊢ φ.comp TensorProduct.includeRight.toRingHom = ↑TensorProduct.includeRight

Tactic:
ext; simp [φ]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv

Tactic:
simp_rw [left_triangle]

Goal state after:
B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫ ((λ_ f₁).hom ≫ (ρ_ f₁).inv) ▷ f₂ ⊗≫ f₁ ◁ ((λ_ f₂).hom ≫ (ρ_ f₂).inv) ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv
Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation

Goal state before:
pp: R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Algebra.FinitePresentation R S
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Module.Finite R R'
w✝¹ : Free R R'
w✝ : Algebra.FinitePresentation R R'
f : R' →ₐ[R] S
hf : Function.Surjective ⇑f
this✝¹ : Algebra R' S := f.toAlgebra
this✝ : IsScalarTower R R' S
this : FinitePresentation R R'
⊢ FinitePresentation R S

Tactic:
have : Module.FinitePresentation R' S :=
    Module.finitePresentation_of_surjective (Algebra.linearMap R' S) hf
      (Algebra.FinitePresentation.ker_fG_of_surjective f hf)

Goal state after:
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Algebra.FinitePresentation R S
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Module.Finite R R'
w✝¹ : Free R R'
w✝ : Algebra.FinitePresentation R R'
f : R' →ₐ[R] S
hf : Function.Surjective ⇑f
this✝² : Algebra R' S := f.toAlgebra
this✝¹ : IsScalarTower R R' S
this✝ : FinitePresentation R R'
this : FinitePresentation R' S
⊢ FinitePresentation R S
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
x✝ : Surjective f
x : ↥X
⊢ 1 (f x) ≤ finrank f (f x)

Tactic:
exact one_le_finrank_map f x

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
n : ℕ
⊢ ord R (x ^ n) = n • ord R x

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, ord_mul, ih, succ_nsmul]
    exact hx

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case pos.top.top
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (⊤ + ⊤) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤

pp: case pos.top.coe
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
a✝ : ℕ
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (⊤ + ↑a✝) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝

pp: case pos.coe.top
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
a✝ : ℕ
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (↑a✝ + ⊤) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤

Tactic:
all_goals simp

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case top
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
y : ↥(nonZeroDivisors R)
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤ = 0 ↔ ⊤ = ⊤

pp: case coe
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
y : ↥(nonZeroDivisors R)
a✝ : ℕ
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝ = 0 ↔ ↑a✝ = ⊤

Tactic:
all_goals simp

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

Goal state before:
pp: ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
inst✝¹ : SetLike ψ C
inst✝ : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
n : ℕ
f : 𝒜 →+*ᵍ 𝒜
⊢ (⇑f)^[n] = ⇑(npowRec n f)

Tactic:
induction n

Goal state after:
case zero
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
inst✝¹ : SetLike ψ C
inst✝ : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
f : 𝒜 →+*ᵍ 𝒜
⊢ (⇑f)^[0] = ⇑(npowRec 0 f)

case succ
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
inst✝¹ : SetLike ψ C
inst✝ : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
f : 𝒜 →+*ᵍ 𝒜
n✝ : ℕ
a✝ : (⇑f)^[n✝] = ⇑(npowRec n✝ f)
⊢ (⇑f)^[n✝ + 1] = ⇑(npowRec (n✝ + 1) f)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
V U : Opens ↑(ProjectiveSpectrum.top 𝒜)
i : V ⟶ U
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
j : ℕ
r s : ↥(𝒜 j)
h : ∀ (x : ↥U), ↑s ∉ (↑x).asHomogeneousIdeal
w : ∀ (x : ↥U), f x = HomogeneousLocalization.mk { deg := j, num := r, den := s, den_mem := ⋯ }
⊢ IsFraction fun x ↦ f (i x)

Tactic:
exact ⟨j, r, s, (h <| i ·), (w <| i ·)⟩

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✝ : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ (Setoid.ker (embedding 𝒜 x)) (-c1) (-c2)

Tactic:
by
    change Localization.mk _ _ = Localization.mk _ _
    simp only [num_neg, den_neg, ← Localization.neg_mk]
    exact congr_arg Neg.neg h

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
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact (pbo (x.num : A)).2.preimage continuous_subtype_val

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 𝒜
x : Submonoid A
n : ℕ
⊢ n.unaryCast.val = ↑n

Tactic:
induction n

Goal state after:
case zero
ι : 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
⊢ (Nat.unaryCast 0).val = ↑0

case succ
ι : 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
n✝ : ℕ
a✝ : n✝.unaryCast.val = ↑n✝
⊢ (n✝ + 1).unaryCast.val = ↑(n✝ + 1)
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
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun x ↦ f ^ x) n ∈ 𝒜 N
hfn : f ^ n = 0
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := N, num := ⟨s, hs⟩, den := ⟨(fun x ↦ f ^ x) n, hn⟩, den_mem := ⋯ }

Tactic:
have := HomogeneousLocalization.subsingleton 𝒜 (x := .powers f) ⟨n, hfn⟩

Goal state after:
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
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun x ↦ f ^ x) n ∈ 𝒜 N
hfn : f ^ n = 0
this : Subsingleton (HomogeneousLocalization 𝒜 (Submonoid.powers f))
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := N, num := ⟨s, hs⟩, den := ⟨(fun x ↦ f ^ x) n, hn⟩, den_mem := ⋯ }
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 : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
a : ↑(CommRingCat.of (Away 𝒜 f))
i : ↑(ProjectiveSpectrum.top 𝒜)
hi : i ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
⊢ val (↑((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x)) a) ⟨i, hi⟩) =
    val (↑((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE ⋯).op)) a) ⟨i, hi⟩)

Tactic:
obtain ⟨⟨n, a, ⟨b, hb'⟩, i, rfl : _ = b⟩, rfl⟩ := mk_surjective a

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i✝ : ↑(ProjectiveSpectrum.top 𝒜)
hi : i✝ ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun x ↦ f ^ x) i ∈ 𝒜 n
⊢ val
      (↑((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x))
            (mk { deg := n, num := a, den := ⟨(fun x ↦ f ^ x) i, hb'⟩, den_mem := ⋯ }))
        ⟨i✝, hi⟩) =
    val
      (↑((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE ⋯).op))
            (mk { deg := n, num := a, den := ⟨(fun x ↦ f ^ x) i, hb'⟩, den_mem := ⋯ }))
        ⟨i✝, hi⟩)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : ModuleCat ↑R
s : Set ↑M
hs : Submodule.span (↑R) s = ⊤
t : Set (↑s →₀ ↑R)
ht : Submodule.span (↑R) t = (Finsupp.linearCombination (↑R) Subtype.val).ker
H₁ :
  Function.Exact ⇑(ConcreteCategory.hom (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)))
    ⇑(ConcreteCategory.hom (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)))
⊢ IsColimit
    (CokernelCofork.ofπ
      ((tildeFinsupp ↑s).inv ≫ tilde.map (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val))) ⋯)

Tactic:
letI h₁ := ModuleCat.isColimitCokernelCofork _ _ H₁
    (by simp [← LinearMap.range_eq_top, Finsupp.range_linearCombination, hs])

Goal state after:
R : CommRingCat
M : ModuleCat ↑R
s : Set ↑M
hs : Submodule.span (↑R) s = ⊤
t : Set (↑s →₀ ↑R)
ht : Submodule.span (↑R) t = (Finsupp.linearCombination (↑R) Subtype.val).ker
H₁ :
  Function.Exact ⇑(ConcreteCategory.hom (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)))
    ⇑(ConcreteCategory.hom (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)))
h₁ : IsColimit (CokernelCofork.ofπ (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)) ⋯) :=
  ModuleCat.isColimitCokernelCofork (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val))
    (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)) H₁ ⋯
⊢ IsColimit
    (CokernelCofork.ofπ
      ((tildeFinsupp ↑s).inv ≫ tilde.map (ModuleCat.ofHom (Finsupp.linearCombination (↑R) 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
⊢ Continuous (FromSpec.toFun f_deg hm)

Tactic:
by
      rw [isTopologicalBasis_subtype (ProjectiveSpectrum.isTopologicalBasis_basic_opens 𝒜)
        (· ∈ pbo f) |>.continuous_iff]
      rintro s ⟨_, ⟨a, rfl⟩, rfl⟩
      have h₁ : Subtype.val (p := (· ∈ pbo f)) ⁻¹' (pbo a) =
          ⋃ i : ℕ, Subtype.val (p := (· ∈ pbo f)) ⁻¹' (pbo (decompose 𝒜 a i)) := by
        simp [ProjectiveSpectrum.basicOpen_eq_union_of_projection 𝒜 a]
      let e : _ ≃ _ :=
        ⟨FromSpec.toFun f_deg hm, ToSpec.toFun f, toSpec_fromSpec _ _ _, fromSpec_toSpec _ _ _⟩
      change IsOpen <| e ⁻¹' _
      rw [← Equiv.image_symm_eq_preimage, h₁, Set.image_iUnion]
      exact isOpen_iUnion fun i ↦ toSpec.image_basicOpen_eq_basicOpen f_deg hm a i ▸
        PrimeSpectrum.isOpen_basicOpen

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

Goal state before:
pp: P Q : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
⊢ ∀ ⦃X : Over S⦄ (S_1 : Presieve X) (Ti : ⦃Y : Over S⦄ → (f : Y ⟶ X) → S_1 f → Presieve Y),
    S_1 ∈ {R | ∃ 𝒰 x, R = 𝒰.toPresieveOver} →
      (∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : S_1 f), Ti f H ∈ {R | ∃ 𝒰 x, R = 𝒰.toPresieveOver}) →
        S_1.bind Ti ∈ {R | ∃ 𝒰 x, R = 𝒰.toPresieveOver}

Tactic:
rintro X _ T ⟨𝒰, h, rfl⟩ H

Goal state after:
P Q : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S 𝒰
T : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver f → Presieve Y
H : ∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOver f), T f H ∈ {R | ∃ 𝒰 x, R = 𝒰.toPresieveOver}
⊢ 𝒰.toPresieveOver.bind T ∈ {R | ∃ 𝒰 x, R = 𝒰.toPresieveOver}
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
⊢ Sieve.functorPushforward F
      ({ 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 := ⋯ }.sieve₁₀
        p₁ p₂) ∈
    J (F.obj W₀)

Tactic:
refine J.superset_covering ?_
          (IsCoverDense.functorPullback_pushforward_covering
            ⟨_, J.pullback_stable (pullback.lift _ _ hp) (hf (pullback (f _ i) (f _ j)))⟩)

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✝³ : 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
⊢ Sieve.functorPushforward F
      (Sieve.functorPullback F
        ↑⟨Sieve.pullback (pullback.lift (F.map p₁) (F.map p₂) hp)
              (Sieve.ofArrows (fun i_1 ↦ F.obj (U (pullback (f S i) (f S j)) i_1)) (f (pullback (f S i) (f S j)))),
            ⋯⟩) ≤
    Sieve.functorPushforward F
      ({ 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 := ⋯ }.sieve₁₀
        p₁ p₂)
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
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
h :
  ((fun Z g hg ↦
          Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
            (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯))))
        V b hb).arrows
    a
⊢ (data.toPreOneHypercover.sieve₁ p₁ p₂).arrows (a ≫ b)

Tactic:
let str := Presieve.getFunctorPushforwardStructure hb.bindStruct.hg

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✝ : 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
h :
  ((fun Z g hg ↦
          Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
            (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯))))
        V b hb).arrows
    a
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 ⋯
⊢ (data.toPreOneHypercover.sieve₁ p₁ p₂).arrows (a ≫ b)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case e'_4.succ
σ : 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₀
n✝ : ℕ
h : d j = n✝ + 1
⊢ a * d i₀ * (n✝ + 1) = a * d i₀ + a * (n✝ + 1 - 1) * d i₀

Tactic:
simp only [add_tsub_cancel_right]; ring

Goal state after: