mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ MonoidHom.mker (ordFrac R) = Submonoid.map (algebraMap R K) (IsUnit.submonoid R)

Tactic:
ordFrac_eq_inverse_comp_valuation,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ MonoidHom.mker
      (MonoidWithZero.inverse.comp (valuation K (IsDiscreteValuationRing.maximalIdeal R)).toMonoidWithZeroHom) =
    Submonoid.map (algebraMap R K) (IsUnit.submonoid R)
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
g : (j₀ : 𝒰.I₀) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.X j₀
hg :
  ∀ (j₀ : 𝒰.I₀) (x : { i // j i = j₀ }),
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ ↑(R ↑x)) x)) ≫ g j₀ = IsOpenImmersion.lift (𝒰.f j₀) (f ↑x) ⋯
R' : 𝒰.I₀ → CommRingCat := fun j₀ ↦ CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))
x✝ : (j₀ : 𝒰.I₀) → ↑(R' j₀)
j₀ : 𝒰.I₀
i : { i // j i = j₀ }
⊢ (fun f x i ↦ f ↑i) ((fun f i ↦ f (j i) ⟨i, ⋯⟩) x✝) j₀ i = x✝ j₀ i

Tactic:
by rcases i with ⟨i, rfl⟩; rfl

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g : A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ zeroLocus 𝒜 {f * g} ↔ x ∈ zeroLocus 𝒜 {f} ∪ zeroLocus 𝒜 {g}

Tactic:
by simpa using x.isPrime.mul_mem_iff_mem_or_mem

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
nonempty : ∀ x ∉ I, {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
ha : antidiag = {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂)) (x * y) =
    (proj 𝒜 max₁) x * (proj 𝒜 max₂) y + ∑ ij ∈ antidiag.erase (max₁, max₂), (proj 𝒜 ij.1) x * (proj 𝒜 ij.2) y
i j : ι
H₁ : ¬(i = max₁ ∧ j = max₂)
H₄ : i + j = max₁ + max₂
H₂ : i ∈ DFinsupp.support ((decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support ((decompose 𝒜) y)
⊢ max₁ < i ∨ max₂ < j

Tactic:
convert! le_or_lt_of_add_le_add H₄.ge using 1

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := ⋯
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₂ : Finset ι := ⋯
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
nonempty : ∀ x ∉ I, {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty
max₁ : ι := ⋯
max₂ : ι := ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) := ⋯
ha : antidiag = {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂)) (x * y) =
    (proj 𝒜 max₁) x * (proj 𝒜 max₂) y + ∑ ij ∈ antidiag.erase (max₁, max₂), (proj 𝒜 ij.1) x * (proj 𝒜 ij.2) y
i j : ι
H₁ : ¬(i = max₁ ∧ j = max₂)
H₄ : i + j = max₁ + max₂
H₂ : i ∈ DFinsupp.support ((decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support ((decompose 𝒜) y)
⊢ max₁ < i ↔ max₁ ≤ i
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: case homogeneous_mem_or_mem.refine_1
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal
H : x ∈ I ∨ y ∈ I
⊢ x ∈ I → x ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal

Tactic:
exact Ideal.mem_homogeneousCore_of_homogeneous_of_mem hx

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:
rw [ToSpec.preimage_basicOpen]

Goal state after:
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)
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 := ⋯ } ∈
    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:
apply Submodule.subset_span
      refine ⟨j, ai, H.trans ?_, ?_⟩
      · exact DirectSum.degree_eq_of_mem_mem 𝒜 hb'
          (SetLike.pow_mem_graded j hf) hfj
      · ext
        simp only [val_mk, Away.val_mk]
        congr
        refine (DirectSum.decompose_of_mem_same _ ?_).symm
        exact H ▸ SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
⊢ ∀ (s : Set (ProjectiveSpectrum 𝒜)), IsClosed s → IsClosed (comapFun f hf ⁻¹' s)

Tactic:
isClosed_iff_zeroLocus,

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
⊢ ∀ (s : Set (ProjectiveSpectrum 𝒜)), (∃ s_1, s = zeroLocus 𝒜 s_1) → ∃ s_1, comapFun f hf ⁻¹' s = zeroLocus ℬ s_1
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 y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ (∀ (x_1 : ℕ),
      HomogeneousLocalization.mk { deg := m * x_1, num := ⟨(proj 𝒜 x_1) x ^ m, ⋯⟩, den := ⟨f ^ x_1, ⋯⟩, den_mem := ⋯ } ∈
        q.asIdeal) ∨
    ∀ (x : ℕ),
      HomogeneousLocalization.mk { deg := m * x, num := ⟨(proj 𝒜 x) y ^ m, ⋯⟩, den := ⟨f ^ x, ⋯⟩, den_mem := ⋯ } ∈
        q.asIdeal

Tactic:
rw [← and_forall_ne nx, and_iff_left, ← and_forall_ne ny, and_iff_left]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ HomogeneousLocalization.mk { deg := m * nx, num := ⟨(proj 𝒜 nx) x ^ m, ⋯⟩, den := ⟨f ^ nx, ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal ∨
    HomogeneousLocalization.mk { deg := m * ny, num := ⟨(proj 𝒜 ny) y ^ m, ⋯⟩, den := ⟨f ^ ny, ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal

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 y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ ∀ (b : ℕ),
    b ≠ ny →
      HomogeneousLocalization.mk { deg := m * b, num := ⟨(proj 𝒜 b) y ^ m, ⋯⟩, den := ⟨f ^ b, ⋯⟩, den_mem := ⋯ } ∈
        q.asIdeal

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 y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ ∀ (b : ℕ),
    b ≠ nx →
      HomogeneousLocalization.mk { deg := m * b, num := ⟨(proj 𝒜 b) x ^ m, ⋯⟩, den := ⟨f ^ b, ⋯⟩, den_mem := ⋯ } ∈
        q.asIdeal
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
⊢ ⇑A.subtype '' ↑I ⊆
    Subtype.val '' ↑(map ((Subring.inclusion ⋯).comp (algebraMap ↥A ↥(LocalSubring.ofPrime A M).toSubring)) M)

Tactic:
refine .trans ?_ (Set.image_mono <| map_mono le)

Goal state after:
K : Type u_3
inst✝ : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
⊢ ⇑A.subtype '' ↑I ⊆
    Subtype.val '' ↑(map ((Subring.inclusion ⋯).comp (algebraMap ↥A ↥(LocalSubring.ofPrime A M).toSubring)) I)
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)
i j : ι
this : Function.Injective ⇑(ConcreteCategory.hom (M.presheaf.map (eqToHom ⋯).op))
⊢ (ConcreteCategory.hom (M.presheaf.map (eqToHom ⋯).op))
      ((ConcreteCategory.hom (M.presheaf.map ⋯.hom.op)) (f ^ K • t i)) =
    (ConcreteCategory.hom (M.presheaf.map (eqToHom ⋯).op))
      ((ConcreteCategory.hom (M.presheaf.map ⋯.hom.op)) (f ^ K • t j))

Tactic:
simp_rw [← M.presheaf.map_comp_apply, ← op_comp, eqToHom_comp_homOfLE]

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 : ι
this : Function.Injective ⇑(ConcreteCategory.hom (M.presheaf.map (eqToHom ⋯).op))
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t 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
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
⊢ data.toPreOneHypercover.sieve₁ p₁ p₂ ∈ J W

Tactic:
have hT : T ∈ J W := J.bind_covering hS (fun Z g hg ↦ by
    apply J.pullback_stable
    rw [Functor.functorPushforward_mem_iff J₀]
    let str := Presieve.getFunctorPushforwardStructure hg.bindStruct.hg
    apply data.mem₁₀
    simp only [str.cover.1.choose_spec, str.cover.2.choose_spec, assoc, w])

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
⊢ data.toPreOneHypercover.sieve₁ p₁ p₂ ∈ J W
Module: Mathlib.AlgebraicGeometry.Sites.Etale

Goal state before:
pp: case refine_2
X : Scheme
W : X.Etale
ι : Type u_1
Z : ι → X.Etale
f : (i : ι) → Z i ⟶ W
hf : ⋃ i, Set.range ⇑(f i).left = Set.univ
i : ↥W.left → ι
z : (w : ↥W.left) → ↥(Z (i w)).left
hz : ∀ (w : ↥W.left), (f (i w)).left (z w) = w
⊢ ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Etale (𝒰.X j ↘ X)), 𝒰.toPresieveOverProp h ≤ (Sieve.ofArrows Z f).arrows

Tactic:
let V : Cover (precoverage @Etale) W.left :=
      Cover.mkOfCovers W.left (fun w ↦ (Z (i w)).left)
        (fun w ↦ (f (i w)).left) (fun w ↦ ⟨_, _, hz w⟩) inferInstance

Goal state after:
case refine_2
X : Scheme
W : X.Etale
ι : Type u_1
Z : ι → X.Etale
f : (i : ι) → Z i ⟶ W
hf : ⋃ i, Set.range ⇑(f i).left = Set.univ
i : ↥W.left → ι
z : (w : ↥W.left) → ↥(Z (i w)).left
hz : ∀ (w : ↥W.left), (f (i w)).left (z w) = w
V : Cover (precoverage @Etale) W.left :=
  Cover.mkOfCovers (↥W.left) (fun w ↦ (Z (i w)).left) (fun w ↦ (f (i w)).left) ⋯ ⋯
⊢ ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Etale (𝒰.X j ↘ X)), 𝒰.toPresieveOverProp h ≤ (Sieve.ofArrows Z f).arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
E : PreZeroHypercover X
hR : E.presieve₀ ∈ P.precoverage.coverings X
F : PreZeroHypercover X
hS : F.presieve₀ ∈ P.precoverage.coverings X
⊢ (E.sum F).presieve₀ ∈ P.precoverage.coverings X

Tactic:
rw [PreZeroHypercover.presieve₀_mem_precoverage_iff] at hR hS ⊢

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
E : PreZeroHypercover X
hR : P.property E
F : PreZeroHypercover X
hS : P.property F
⊢ P.property (E.sum F)
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
right✝ : Finite 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc.sigma
⊢ Presieve.IsSheafFor F 𝒰.forgetQc.presieve₀

Tactic:
← Scheme.Cover.isSheafFor_sigma_iff hzar,

Goal state after:
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
right✝ : Finite 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc.sigma
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.forgetQc.sigma.X 𝒰.forgetQc.sigma.f)
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
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ Y₀ : C₀
f : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
T₀ : C₀
c : T₀ ⟶ W₀
Y : C
i : (data (F.obj X₀)).I₀
d : F.obj T₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac₂ : d ≫ (data (F.obj X₀)).f i = F.map (c ≫ b)
⊢ inv data G₀ X₀ ≫ presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ d =
    IsDenseSubsite.mapPreimage J F G₀ f ≫ G₀.obj.map (c ≫ a).op

Tactic:
inv_π_assoc,

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
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ Y₀ : C₀
f : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
T₀ : C₀
c : T₀ ⟶ W₀
Y : C
i : (data (F.obj X₀)).I₀
d : F.obj T₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac₂ : d ≫ (data (F.obj X₀)).f i = F.map (c ≫ b)
⊢ IsDenseSubsite.mapPreimage J F G₀ ((data (F.obj X₀)).f i) ≫ IsDenseSubsite.mapPreimage J F G₀ d =
    IsDenseSubsite.mapPreimage J F G₀ f ≫ G₀.obj.map (c ≫ a).op
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type v)
f : J.yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (F.obj.map g.op)) (J.yonedaEquiv f) = J.yonedaEquiv (J.yoneda.map g ≫ f)

Tactic:
simp [yonedaEquiv, CategoryTheory.yonedaEquiv_naturality]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type v)
f : J.yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ CategoryTheory.yoneda.map g ≫ (fullyFaithfulSheafToPresheaf J (Type v)).homEquiv f =
    (fullyFaithfulSheafToPresheaf J (Type v)).homEquiv (J.yoneda.map g ≫ f)
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)
inst✝ : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ j, Subobject.mk (F.obj j).obj.hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun j ↦ (F.obj j).obj.hom, naturality := ⋯ } }
this✝ : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
j : J
⊢ colimit.ι ((F ⋙ MonoOver.forget X) ⋙ Over.forget X) j ≫ Subobject.ofMkLEMk f c.pt.hom ⋯ ≫ c.pt.hom =
    Over.Hom.left (c.ι.app j) ≫ c.pt.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)
inst✝ : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ j, Subobject.mk (F.obj j).obj.hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun j ↦ (F.obj j).obj.hom, naturality := ⋯ } }
this✝ : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
j : J
⊢ colimit.ι ((F ⋙ MonoOver.forget X) ⋙ Over.forget X) j ≫ f = Over.Hom.left (c.ι.app j) ≫ c.pt.hom