mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
⊢ (PrimeSpectrum.zeroLocus ↑(Ideal.span {r})).Nonempty

Tactic:
Set.nonempty_iff_ne_empty,

Goal state after:
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
⊢ PrimeSpectrum.zeroLocus ↑(Ideal.span {r}) ≠ ∅
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
⊢ ringKrullDim R + ↑(ENat.card σ) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
cases finite_or_infinite σ

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Finite σ
⊢ ringKrullDim R + ↑(ENat.card σ) ≤ ringKrullDim (MvPolynomial σ R)

case inr
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
⊢ ringKrullDim R + ↑(ENat.card σ) ≤ ringKrullDim (MvPolynomial σ R)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ (ρ_ r₁).inv ≫
      (𝟙 (r₁ ≫ 𝟙 c) ⊗≫
          r₁ ◁ 𝟙 c ◁ adj₁.unit ⊗≫
            r₁ ◁ ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ▷ r₁ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₁ ⊗≫ 𝟙 (𝟙 d ≫ r₁)) ≫
        (λ_ r₁).hom =
    𝟙 r₁

Tactic:
calc
    _ = 𝟙 _ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 r₁ := by
      rw [adj₁.right_triangle]
      bicategory

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
⊢ Function.RightInverse
    (fun β ↦
      { hom := (conjugateEquiv adj₁ adj₂).symm β.hom, inv := (conjugateEquiv adj₂ adj₁).symm β.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ })
    fun α ↦
    { hom := (conjugateEquiv adj₁ adj₂) α.hom, inv := (conjugateEquiv adj₂ adj₁) α.inv, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }

Tactic:
intro α
    simp only [Equiv.apply_symm_apply]

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 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ ↑(⨅ x ∈ t, x.asHomogeneousIdeal) ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}

Tactic:
SetLike.mem_coe,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ ⨅ x ∈ t, x.asHomogeneousIdeal ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}
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 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
z : at x
⊢ (ConcreteCategory.hom (stalkToFiberRingHom 𝒜 x)) (homogeneousLocalizationToStalk 𝒜 x z) = z

Tactic:
by
  obtain ⟨z, rfl⟩ := Quotient.mk''_surjective z
  rw [homogeneousLocalizationToStalk, Quotient.liftOn'_mk'',
    stalkToFiberRingHom_germ, sectionInBasicOpen]

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

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
⊢ g ^ e * f ^ (2 * e + d) ∈ 𝒜 ((d + e) • (d + e))

Tactic:
convert!
        SetLike.mul_mem_graded (SetLike.pow_mem_graded e hg)
          (SetLike.pow_mem_graded (2 * e + d) hf) using 2
      ring

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

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : 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
⊢ (IsLocalization.map (Localization (↑⟨i✝, hi⟩).asHomogeneousIdeal.toIdeal.primeCompl) (RingHom.id A) ⋯)
      (val ((awayMap 𝒜 g_deg hx) (mk { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }))) =
    val
      (↑((CommRingCat.Hom.hom ((Proj 𝒜).presheaf.map (homOfLE ⋯).op))
            ((CommRingCat.Hom.hom (awayToSection 𝒜 f)) (mk { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ })))
        ⟨i✝, hi⟩)

Tactic:
val_awayMap_mk,

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
⊢ (IsLocalization.map (Localization (↑⟨i✝, hi⟩).asHomogeneousIdeal.toIdeal.primeCompl) (RingHom.id A) ⋯)
      (Localization.mk (↑a * g ^ i) ⟨x ^ i, ⋯⟩) =
    val
      (↑((CommRingCat.Hom.hom ((Proj 𝒜).presheaf.map (homOfLE ⋯).op))
            ((CommRingCat.Hom.hom (awayToSection 𝒜 f)) (mk { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ })))
        ⟨i✝, hi⟩)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
N : ModuleCat ↑(CommRingCat.of ↑R) := (modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)
n : ℕ
a : ↑R
e : unop g ^ n = unop f * a
⊢ IsUnit
    ((algebraMap (↑R)
        (Module.End ↑R ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).obj g)))
      (unop f * a))

Tactic:
← e,

Goal state after:
case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
N : ModuleCat ↑(CommRingCat.of ↑R) := (modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)
n : ℕ
a : ↑R
e : unop g ^ n = unop f * a
⊢ IsUnit
    ((algebraMap (↑R)
        (Module.End ↑R ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).obj g)))
      (unop g ^ n))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1
X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
I : Type u
W : I → TopologicalSpace.Opens ↥X
cov : (Opens.grothendieckTopology ↥X).CoversTop W
pres : (i : I) → (SheafOfModules.over M (W i)).Presentation
κ : I → Set (TopologicalSpace.Opens ↥X)
hsub : ∀ (i : I), κ i ⊆ X.affineOpens
heq : ∀ (i : I), W i = sSup (κ i)
i : (i : I) × ↑(κ i)
u : ↑↑i.snd ⟶ ↑(W i.fst) := X.homOfLE ⋯
this : PreservesColimitsOfSize.{u, u, u, u, u + 1, u + 1} (restrictFunctor u)
F : SheafOfModules (Sheaf.over X.ringCatSheaf (W i.fst)) ⥤ (↑↑i.snd).Modules :=
  (overEquiv (W i.fst)).functor ⋙ restrictFunctor u
iso : SheafOfModules.overFunctor X.ringCatSheaf (W i.fst) ⋙ F ≅ restrictFunctor (Opens.ι ↑i.snd) :=
  ((SheafOfModules.overFunctor X.ringCatSheaf (W i.fst)).associator (overEquiv (W i.fst)).functor
        (restrictFunctor u)).symm ≪≫
    Functor.isoWhiskerRight (overFunctorEquiv (W i.fst)) (restrictFunctor u) ≪≫
      (restrictFunctorComp u (Opens.ι (W i.fst))).symm ≪≫ restrictFunctorCongr ⋯
⊢ SheafOfModules.Presentation (M.restrict (Opens.ι ((fun j ↦ ↑j.snd) i)))

Tactic:
exact SheafOfModules.Presentation.ofIsIso.{u, u, u} (iso.app M).hom <|
      (pres i.1).map F (Scheme.Modules.restrictUnitIso _).symm

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

Goal state before:
pp: case refine_2
K : Type u_3
inst✝ : Field K
A✝ : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A✝
H : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x ↦ ↑x)
A : LocalSubring K
hA : A ∈ s
a : K
haA : a ∈ A.toSubring
h : IsUnit ((Subring.inclusion ⋯) ⟨a, haA⟩)
b : K
hb : b ∈ { toSubring := ⨆ i, (↑i).toSubring, isLocalRing := ⋯ }.toSubring
e : (Subring.inclusion ⋯) ⟨a, haA⟩ * ⟨b, hb⟩ = 1
B : { a // a ∈ s }
hbB : b ∈ (↑B).toSubring
⊢ IsUnit ⟨a, haA⟩

Tactic:
obtain ⟨C, hCA, hCB⟩ := H.directed ⟨A, hA⟩ B

Goal state after:
case refine_2
K : Type u_3
inst✝ : Field K
A✝ : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A✝
H : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x ↦ ↑x)
A : LocalSubring K
hA : A ∈ s
a : K
haA : a ∈ A.toSubring
h : IsUnit ((Subring.inclusion ⋯) ⟨a, haA⟩)
b : K
hb : b ∈ { toSubring := ⨆ i, (↑i).toSubring, isLocalRing := ⋯ }.toSubring
e : (Subring.inclusion ⋯) ⟨a, haA⟩ * ⟨b, hb⟩ = 1
B : { a // a ∈ s }
hbB : b ∈ (↑B).toSubring
C : { a // a ∈ s }
hCA : (fun x ↦ ↑x) ⟨A, hA⟩ ≤ (fun x ↦ ↑x) C
hCB : (fun x ↦ ↑x) B ≤ (fun x ↦ ↑x) C
⊢ IsUnit ⟨a, haA⟩
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
V : ValuationSubring K := { toSubring := (algebraMap R K).range, mem_or_inv_mem' := ⋯ }
this : LocalSubring.range g ≤ V.toLocalSubring
⊢ Function.Surjective ⇑(g.rangeRestrict.comp f)

Tactic:
by
      rintro ⟨_, x, rfl⟩
      obtain ⟨y, hy⟩ := this.1 ⟨x, rfl⟩
      exact ⟨y, Subtype.ext (by simpa [← h] using hy)⟩

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

Goal state before:
pp: case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.I₀
h : V ⟶ 𝒰.X k
hcomp : h ≫ 𝒰.f k = f
⊢ ∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯

Tactic:
have : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S := comp_over (𝒰.f k) S

Goal state after:
case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.I₀
h : V ⟶ 𝒰.X k
hcomp : h ≫ 𝒰.f k = f
this : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S
⊢ ∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case intro
σ : 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
⊢ ∃ j₀ φ', φ'.comp (awayMap 𝒜 ⋯ ⋯) = φ ∧ (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range

Tactic:
have hi₀ (j) : ψ j ≤ ψ i₀ := hi1 ▸ (Finset.univ.image ψ).le_max' (ψ j) (by simp)

Goal state after:
case intro
σ : 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₀
⊢ ∃ j₀ φ', φ'.comp (awayMap 𝒜 ⋯ ⋯) = φ ∧ (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
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 : (data X).I₀
⊢ ∀ ⦃I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨Sieve.functorPullback F (Sieve.pullback ((data X).f i) ↑S), ⋯⟩⦄
    (r : I₁.Relation I₂),
    (match I₁ with
        | { Y := W₀, f := a, hf := ha } => s.ι { Y := F.obj W₀, f := F.map a ≫ (data X).f i, hf := ha }) ≫
        (F.op ⋙ G).map r.g₁.op =
      (match I₂ with
        | { Y := W₀, f := a, hf := ha } => s.ι { Y := F.obj W₀, f := F.map a ≫ (data X).f i, hf := ha }) ≫
        (F.op ⋙ G).map r.g₂.op

Tactic:
rintro ⟨W₀, a, ha⟩ ⟨Z₀, b, hb⟩ ⟨U₀, p₁, p₂, fac⟩
      exact s.condition
        { fst := ⟨_, _, ha⟩
          snd := ⟨_, _, hb⟩
          r := ⟨_, F.map p₁, F.map p₂, by
              simp only [← Functor.map_comp_assoc, fac]⟩ }

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

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
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 : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
W₀ : C₀
a : W₀ ⟶ T₀
q₁ : W₀ ⟶ (data X).X h₁.i₀
w₁ : F.map q₁ = F.map a ≫ F.map p₁ ≫ h₁.q
q₂ : W₀ ⟶ (data X).X h₂.i₀
w₂ : F.map q₂ = F.map a ≫ F.map p₂ ≫ h₂.q
⊢ F.map q₁ ≫ (data X).f h₁.i₀ = F.map q₂ ≫ (data X).f h₂.i₀

Tactic:
simp only [w₁, w₂, assoc, h₁.fac, h₂.fac, ← Functor.map_comp_assoc, w]

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

Goal state before:
pp: P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ propQCPrecoverage P ≤ propQCPrecoverage Q

Tactic:
propQCPrecoverage,

Goal state after:
P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ qcPrecoverage ⊓ precoverage P ≤ propQCPrecoverage Q
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
⊢ zariskiPrecoverage ≤ propQCPrecoverage P

Tactic:
propQCPrecoverage,

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
⊢ zariskiPrecoverage ≤ qcPrecoverage ⊓ precoverage P
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: case refine_3.inr.refine_2
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))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
⊢ ∀ ⦃i j : T.affineOneHypercover.I₀⦄ (k : T.affineOneHypercover.I₁ i j),
    Presieve.IsSeparatedFor F
      (Sieve.pullback (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) (Sieve.generate 𝒰.presieve₀)).arrows

Tactic:
intro i j k
        rw [← Sieve.pullbackArrows_comm, ← Presieve.isSeparatedFor_iff_generate]
        apply Presieve.IsSheafFor.isSeparatedFor
        rw [← Presieve.ofArrows_pullback]
        exact this (𝒰.pullback₂ _) ⟨_, rfl⟩

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

Goal state before:
pp: ⊢ fppfPrecoverage ≤ propQCPrecoverage @Flat

Tactic:
propQCPrecoverage,

Goal state after:
⊢ fppfPrecoverage ≤ qcPrecoverage ⊓ precoverage @Flat
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: A : Type v
inst✝² : TopologicalSpace A
inst✝¹ : AddCommGroup A
inst✝ : IsTopologicalAddGroup A
⊢ Presheaf.IsSheaf Scheme.fpqcTopology (continuousMapPresheafAb A)

Tactic:
apply Presheaf.isSheaf_of_isSheaf_comp _ _ (forget Ab)
  exact isSheaf_fpqcTopology_continuousMapPresheaf _

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

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁸ : P.IsStableUnderComposition
K : Precoverage C
inst✝⁷ : K.HasIsos
inst✝⁶ : K.IsStableUnderBaseChange
inst✝⁵ : K.IsStableUnderComposition
inst✝⁴ : K.HasPullbacks
inst✝³ : HasFiniteWidePullbacks C
inst✝² : P.HasOfPostcompProperty P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.ContainsIdentities
H : K ≤ P.precoverage
this : RepresentablyFlat (Over.forget P ⊤ S)
⊢ (Over.forget P ⊤ S).IsContinuous
    (Precoverage.comap (Over.forget P ⊤ S ⋙ CategoryTheory.Over.forget S) K).toGrothendieck (K.toGrothendieck.over S)

Tactic:
Functor.isContinuous_iff_coverPreserving

Goal state after:
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁸ : P.IsStableUnderComposition
K : Precoverage C
inst✝⁷ : K.HasIsos
inst✝⁶ : K.IsStableUnderBaseChange
inst✝⁵ : K.IsStableUnderComposition
inst✝⁴ : K.HasPullbacks
inst✝³ : HasFiniteWidePullbacks C
inst✝² : P.HasOfPostcompProperty P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.ContainsIdentities
H : K ≤ P.precoverage
this : RepresentablyFlat (Over.forget P ⊤ S)
⊢ CoverPreserving (Precoverage.comap (Over.forget P ⊤ S ⋙ CategoryTheory.Over.forget S) K).toGrothendieck
    (K.toGrothendieck.over S) (Over.forget P ⊤ S)
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 : C
i : (data X).I₀
j : (data (F.obj ((data X).X i))).I₀
⊢ restriction data G₀ ((data (F.obj ((data X).X i))).f j ≫ (data X).f i) =
    presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ ((data (F.obj ((data X).X i))).f j)

Tactic:
apply restriction_eq_of_fac

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 : C
i : (data X).I₀
j : (data (F.obj ((data X).X i))).I₀
⊢ (data (F.obj ((data X).X i))).f j ≫ (data X).f i = (data (F.obj ((data X).X i))).f j ≫ (data X).f i
Module: Mathlib.AlgebraicGeometry.Sites.Proetale

Goal state before:
pp: ⊢ etalePrecoverage ≤ propQCPrecoverage @WeaklyEtale

Tactic:
propQCPrecoverage,

Goal state after:
⊢ etalePrecoverage ≤ qcPrecoverage ⊓ precoverage @WeaklyEtale
Module: Mathlib.AlgebraicGeometry.Sites.Proetale

Goal state before:
pp: S : Scheme
⊢ (ProEt.forget S).IsContinuous (topology S) (proetaleTopology.over S)

Tactic:
Functor.isContinuous_iff_coverPreserving

Goal state after:
S : Scheme
⊢ CoverPreserving (topology S) (proetaleTopology.over S) (ProEt.forget S)
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
⊢ HasColimitsOfShape α C

Tactic:
by_cases hf : Function.Surjective f
  · exact hasColimitsOfShape_of_equivalence
      (OrderIso.ofRelIsoLT (RelIso.ofSurjective f.toRelEmbedding hf)).equivalence.symm
  · let s := f.toPrincipalSeg hf
    obtain ⟨i, hi₀⟩ : ∃ i, i = s.top := ⟨_, rfl⟩
    induction i using SuccOrder.limitRecOn with
    | isMin i hi =>
      subst hi₀
      exact (hi.not_lt (s.lt_top (Classical.arbitrary _))).elim
    | succ i hi _ =>
      obtain ⟨a, rfl⟩ := (s.mem_range_iff_rel (b := i)).2 (by
        simpa only [← hi₀] using Order.lt_succ_of_not_isMax hi)
      have : OrderTop α :=
        { top := a
          le_top b := by
            rw [← s.le_iff_le]
            exact Order.le_of_lt_succ (by simpa only [hi₀] using s.lt_top b) }
      infer_instance
    | isSuccLimit i hi =>
      subst hi₀
      exact hasColimitsOfShape_of_isSuccLimit' C s hi

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
ι : Type w
X Y : C
F₁ F₂ : Discrete ι ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
φ : F₁ ⟶ F₂
hφ : (ofHoms g).functorCategory (Discrete ι) φ
g₁ : c₁.pt ⟶ X₁
g₂ : { pt := c₂.pt, ι := φ ≫ c₂.ι }.pt ⟶ X₂
sq : IsPushout g₁ (h₁.desc { pt := c₂.pt, ι := φ ≫ c₂.ι }) f g₂
π : ι → α := fun i ↦ ⋯.choose
⊢ Nonempty (AttachCells g f)

Tactic:
let e (i : ι) : Arrow.mk (φ.app ⟨i⟩) ≅ Arrow.mk (g (π i)) :=
      eqToIso (((ofHoms_iff _ _).1 (hφ ⟨i⟩)).choose_spec)

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
ι : Type w
X Y : C
F₁ F₂ : Discrete ι ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
φ : F₁ ⟶ F₂
hφ : (ofHoms g).functorCategory (Discrete ι) φ
g₁ : c₁.pt ⟶ X₁
g₂ : { pt := c₂.pt, ι := φ ≫ c₂.ι }.pt ⟶ X₂
sq : IsPushout g₁ (h₁.desc { pt := c₂.pt, ι := φ ≫ c₂.ι }) f g₂
π : ι → α := fun i ↦ ⋯.choose
e : (i : ι) → Arrow.mk (φ.app { as := i }) ≅ Arrow.mk (g (π i)) := fun i ↦ eqToIso ⋯
⊢ Nonempty (AttachCells g f)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case neg
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ : J
h₀ : j ≤ Order.succ j
hj₂ : restrictionLE iter₁.F h₀ = restrictionLE iter₂.F h₀
hsucc : iter₁.F.obj ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), k₂ ≤ j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
h₁₂ : k₁ ≤ Order.succ j
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h' : ¬k₁ ≤ j
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂

Tactic:
simp only [not_le] at h'

Goal state after:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ : J
h₀ : j ≤ Order.succ j
hj₂ : restrictionLE iter₁.F h₀ = restrictionLE iter₂.F h₀
hsucc : iter₁.F.obj ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), k₂ ≤ j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
h₁₂ : k₁ ≤ Order.succ j
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h' : j < k₁
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂