mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.FiniteType

Goal state before:
pp: S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
n : S → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
⊢ ∀ i ∈ {x ∈ s | n x ≠ 0}, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n

Tactic:
by simpa using fun i hi hin ↦ ⟨n i, hin, hn i hi⟩

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✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
c : NumDenSameDeg 𝒜 x
n : ℕ
⊢ ↑(GradedMonoid.GMonoid.gnpow n c.den) ∈ x

Tactic:
induction n with
        | zero => simp only [coe_gnpow, pow_zero, one_mem]
        | succ n ih => simpa only [pow_succ, coe_gnpow] using x.mul_mem ih c.den_mem

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
𝒜 : ι → σ
x : Submonoid A
f : HomogeneousLocalization 𝒜 x
⊢ f.den • f.val = (algebraMap A (at x)) f.num

Tactic:
rw [eq_num_div_den, Localization.mk_eq_mk', IsLocalization.smul_mk']
  exact IsLocalization.mk'_mul_cancel_left _ ⟨_, _⟩

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

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
U : (Spec R).Opens
f : ↑R
hle : U ≤ PrimeSpectrum.basicOpen f
⊢ IsSMulRegular (↑Γ(M, U)) f

Tactic:
intro x y hxy
  have := M.isUnit_algebraMap_end_of_le_basicOpen _ hle
  rw [Module.End.isUnit_iff] at this
  exact this.injective hxy

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

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
U : (Spec R).Opens
f : ↑R
hle : U ≤ PrimeSpectrum.basicOpen f
⊢ IsSMulRegular (↑Γ(M, U)) f

Tactic:
by
  intro x y hxy
  have := M.isUnit_algebraMap_end_of_le_basicOpen _ hle
  rw [Module.End.isUnit_iff] at this
  exact this.injective hxy

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

Goal state before:
pp: A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
⊢ CommRingCat.ofHom
      (localRingHom f ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal p.asHomogeneousIdeal.toIdeal ⋯) =
    ((stalkIso 𝒜 ((ProjectiveSpectrum.comap f hf) p)).inv ≫ PresheafedSpace.Hom.stalkMap (sheafedSpaceMap f hf).hom p) ≫
      (stalkIso ℬ p).hom

Tactic:
ext : 1

Goal state after:
A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
⊢ CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (localRingHom f ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal p.asHomogeneousIdeal.toIdeal
          ⋯)) =
    CommRingCat.Hom.hom
      (((stalkIso 𝒜 ((ProjectiveSpectrum.comap f hf) p)).inv ≫
          PresheafedSpace.Hom.stalkMap (sheafedSpaceMap f hf).hom p) ≫
        (stalkIso ℬ p).hom)
Module: Mathlib.RingTheory.LocalRing.LocalSubring

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ Function.Injective toSubring

Tactic:
by
  rintro ⟨a, b⟩ ⟨c, d⟩ rfl; rfl

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

Goal state before:
pp: X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
ι : Type u
U : ι → X.Opens
pres : (i : ι) → SheafOfModules.Presentation (M.restrict (U i).ι)
hU : IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
⊢ ∃ 𝒰, ∀ (i : 𝒰.I₀), Nonempty (SheafOfModules.Presentation (M.restrict (𝒰.f i)))

Tactic:
refine ⟨Scheme.AffineOpenCover.ofIsOpenCover _ hU hU', fun i ↦ ⟨?_⟩⟩

Goal state after:
X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
ι : Type u
U : ι → X.Opens
pres : (i : ι) → SheafOfModules.Presentation (M.restrict (U i).ι)
hU : IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
i : (AffineOpenCover.ofIsOpenCover U hU hU').I₀
⊢ SheafOfModules.Presentation (M.restrict ((AffineOpenCover.ofIsOpenCover U hU hU').f i))
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
⊢ ∃ R', R'.toLocalSubring = R

Tactic:
suffices ∀ x ∉ R.toSubring, x⁻¹ ∈ R.toSubring from
    ⟨⟨R.toSubring, fun x ↦ or_iff_not_imp_left.mpr (this x)⟩, rfl⟩

Goal state after:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
⊢ ∀ x ∉ R.toSubring, x⁻¹ ∈ R.toSubring
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: 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
⊢ y ∈ s → ∃ ub, ∀ z ∈ s, z ≤ ub

Tactic:
hys

Goal state after:
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
⊢ ∃ ub, ∀ z ∈ s, z ≤ ub
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 𝒜
x : ↑Proj.T
⊢ ∃ f m, ∃ (_ : f ∈ 𝒜 m) (_ : 0 < m), f ∉ x.asHomogeneousIdeal

Tactic:
by_contra!
      refine x.not_irrelevant_le fun z hz ↦ ?_
      rw [← DirectSum.sum_support_decompose 𝒜 z]
      exact x.1.toIdeal.sum_mem fun k hk ↦ this _ k (SetLike.coe_mem _) <| by_contra <| by aesop

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
this : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S
⊢ Over.homMk h ⋯ ≫ Hom.asOver (𝒰.f k) S = Over.homMk f ⋯

Tactic:
ext : 1

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
⊢ Over.Hom.left (Over.homMk h ⋯ ≫ Hom.asOver (𝒰.f k) S) = Over.Hom.left (Over.homMk f ⋯)
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
⊢ { l := l₁, fac_left := hl₁, fac_right := hl₁' } = { l := l₂, fac_left := hl₂, fac_right := hl₂' }

Tactic:
ext : 1

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
⊢ { l := l₁, fac_left := hl₁, fac_right := hl₁' }.l = { l := l₂, fac_left := hl₂, fac_right := hl₂' }.l
Module: Mathlib.AlgebraicGeometry.Sites.Affine

Goal state before:
pp: S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
U : P.Over ⊤ S
⊢ Sieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U ∈ (smallGrothendieckTopology P S) U

Tactic:
Scheme.mem_smallGrothendieckTopology

Goal state after:
S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
U : P.Over ⊤ S
⊢ ∃ 𝒰 x,
    ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)),
      𝒰.toPresieveOverProp h ≤ (Sieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U).arrows
Module: Mathlib.AlgebraicGeometry.Sites.Affine

Goal state before:
pp: S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
𝒰 : X.left.AffineOpenCover := X.left.affineOpenCover
𝒱 : Cover (precoverage P) X.left := Cover.changeProp 𝒰.openCover ⋯
x✝ : (i : 𝒱.I₀) → (𝒱.X i).Over S := fun i ↦ { hom := 𝒰.f i ≫ X.hom }
this : Cover.Over S 𝒱 := { over := inferInstance, isOver_map := ⋯ }
⊢ (Sieve.ofArrows
      (fun i ↦
        (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj ((fun i ↦ affineOverMk (𝒰.f i ≫ X.hom) ⋯) i))
      fun i ↦ MorphismProperty.CostructuredArrow.homMk (𝒰.f i) ⋯ ⋯) ∈
    (smallGrothendieckTopology P S) X

Tactic:
Scheme.mem_smallGrothendieckTopology

Goal state after:
S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
𝒰 : X.left.AffineOpenCover := X.left.affineOpenCover
𝒱 : Cover (precoverage P) X.left := Cover.changeProp 𝒰.openCover ⋯
x✝ : (i : 𝒱.I₀) → (𝒱.X i).Over S := fun i ↦ { hom := 𝒰.f i ≫ X.hom }
this : Cover.Over S 𝒱 := { over := inferInstance, isOver_map := ⋯ }
⊢ ∃ 𝒰_1 x,
    ∃ (h : ∀ (j : 𝒰_1.I₀), P (𝒰_1.X j ↘ S)),
      𝒰_1.toPresieveOverProp h ≤
        (Sieve.ofArrows
            (fun i ↦
              (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj
                ((fun i ↦ affineOverMk (𝒰.f i ≫ X.hom) ⋯) i))
            fun i ↦ MorphismProperty.CostructuredArrow.homMk (𝒰.f i) ⋯ ⋯).arrows
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
ι : Type u
U : ι → (Spec R).Opens
pres : (i : ι) → SheafOfModules.Presentation (M.restrict (U i).ι)
hU : IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
s : Finset ι
hs : IsOpenCover fun i ↦ U ↑i
⊢ Aux M ⊤

Tactic:
choose κ hκ a ha using fun i : s ↦
    PrimeSpectrum.isBasis_basic_opens.exists_iSup_eq_of_isCompact (U i) (hU' i).isCompact

Goal state after:
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
ι : Type u
U : ι → (Spec R).Opens
pres : (i : ι) → SheafOfModules.Presentation (M.restrict (U i).ι)
hU : IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
s : Finset ι
hs : IsOpenCover fun i ↦ U ↑i
κ : ↥s → Type u
hκ : ∀ (i : ↥s), Finite (κ i)
a : (i : ↥s) → κ i → ↑R
ha : ∀ (i : ↥s), U ↑i = ⨆ k, PrimeSpectrum.basicOpen (a i k)
⊢ Aux M ⊤
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 : PreZeroHypercover X) (F : (i : E.I₀) → PreZeroHypercover (E.X i)),
    P.property E → (∀ (i : E.I₀), P.property (F i)) → P.property (E.bind F)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
σ : ι → Type (max u v)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ P.precoverage.coverings (X i)
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ P.precoverage.coverings S

Tactic:
by
    let E : PreZeroHypercover S := ⟨_, _, f⟩
    let F (i : ι) : PreZeroHypercover (E.X i) := ⟨_, _, g i⟩
    refine (E.bind F).presieve₀_mem_precoverage_iff.mpr (h _ _ ?_ fun i ↦ ?_)
    · rwa [← E.presieve₀_mem_precoverage_iff]
    · rw [← (F i).presieve₀_mem_precoverage_iff]
      exact hg i

Goal state after:
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
⊢ ∀ {Y_1 Z : C} {f_1 : Y_1 ⟶ X}, (∃ e, e ≫ f = f_1) → ∀ (g : Z ⟶ Y_1), ∃ e, e ≫ f = g ≫ f_1

Tactic:
rintro W Z g ⟨e, rfl⟩ q
    exact ⟨q ≫ e, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : EffectiveEpiStruct f
D : Type (max u v) := ⋯
F : D ⥤ C := ⋯
S : Cocone (Sieve.generateSingleton f).arrows.diagram
m : (Sieve.generateSingleton f).arrows.cocone.pt ⟶ S.pt
hm :
  ∀ (j : (Sieve.generateSingleton f).arrows.category), (Sieve.generateSingleton f).arrows.cocone.ι.app j ≫ m = S.ι.app j
h1 : (Sieve.generateSingleton f).arrows (Over.mk f).hom
h2 :
  ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
    g₁ ≫ f = g₂ ≫ f →
      g₁ ≫ S.ι.app { obj := Over.mk f, property := h1 } = g₂ ≫ S.ι.app { obj := Over.mk f, property := h1 }
⊢ f ≫ m = S.ι.app { obj := Over.mk f, property := h1 }

Tactic:
exact hm ⟨Over.mk f, 𝟙 _, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
A : Over X
hA : (Sieve.generateSingleton f).arrows A.hom
B : Over X
hB : (Sieve.generateSingleton f).arrows B.hom
q : A ⟶ B
⊢ (Over.Hom.left q ≫ Exists.choose hB) ≫ e = Exists.choose hA ≫ e

Tactic:
apply h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
A : Over X
hA : (Sieve.generateSingleton f).arrows A.hom
B : Over X
hB : (Sieve.generateSingleton f).arrows B.hom
q : A ⟶ B
⊢ (Over.Hom.left q ≫ Exists.choose hB) ≫ f = Exists.choose hA ≫ f
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => Exists.choose hT ≫ e,
          naturality := ⋯ } }
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
⊢ Exists.choose ⋯ ≫ e = 𝟙 Y ≫ e

Tactic:
apply h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram := ⋯
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
⊢ Exists.choose ⋯ ≫ f = 𝟙 Y ≫ f
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => Exists.choose hT ≫ e,
          naturality := ⋯ } }
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
m : X ⟶ W
hm : f ≫ m = e
A : Over X
g : A.left ⟶ Y
hA : g ≫ f = A.hom
⊢ g ≫ e = (aux e ⋯).ι.app { obj := A, property := ⋯ }

Tactic:
apply h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram := ⋯
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
m : X ⟶ W
hm : f ≫ m = e
A : Over X
g : A.left ⟶ Y
hA : g ≫ f = A.hom
⊢ g ≫ f = ⋯.choose ≫ f
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B✝ : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B✝
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
A : Over B✝
a : α
g₁ : A.left ⟶ X a
ha : g₁ ≫ π a = A.hom
B : Over B✝
b : α
g₂ : B.left ⟶ X b
hb : g₂ ≫ π b = B.hom
q : A ⟶ B
⊢ (Over.Hom.left q ≫ ⋯.choose) ≫ e ⋯.choose = ⋯.choose ≫ e ⋯.choose

Tactic:
apply h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
B✝ : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B✝
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
A : Over B✝
a : α
g₁ : A.left ⟶ X a
ha : g₁ ≫ π a = A.hom
B : Over B✝
b : α
g₂ : B.left ⟶ X b
hb : g₂ ≫ π b = B.hom
q : A ⟶ B
⊢ (Over.Hom.left q ≫ ⋯.choose) ≫ π ⋯.choose = ⋯.choose ≫ π ⋯.choose
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => ⋯.choose ≫ e (Exists.choose hT),
          naturality := ⋯ } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ ⋯.choose ≫ e (Exists.choose ⋯) = 𝟙 (X a) ≫ e a

Tactic:
apply h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram := ⋯
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ ⋯.choose ≫ π (Exists.choose ⋯) = 𝟙 (X a) ≫ π a
Module: Mathlib.AlgebraicGeometry.Sites.Fpqc

Goal state before:
pp: case refine_2
X : Scheme
⊢ ∀ {R S : CommRingCat} (f : R ⟶ S),
    Flat (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor (yoneda.obj X) (Presieve.singleton (Spec.map f))

Tactic:
intro R S f hf₁ hf₂
    have : IsRegularEpi (Spec.map f) :=
      isRegularEpi_of_flat_of_surjective_of_isAffine _
    exact .singleton_of_isRepresentable_of_effectiveEpi _ _

Goal state after:
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => ⋯.choose ≫ e (Exists.choose hT),
          naturality := ⋯ } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
T : Over B
a : α
g : T.left ⟶ X a
ha : g ≫ π a = T.hom
⊢ g ≫ e a = (aux e ⋯).ι.app { obj := T, property := ⋯ }

Tactic:
apply h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram := ⋯
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
T : Over B
a : α
g : T.left ⟶ X a
ha : g ≫ π a = T.hom
⊢ g ≫ π a = ⋯.choose ≫ π ⋯.choose
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

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
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
this : IsFiltered J
⊢ ∃ j φ, y ≫ Y.map φ = 0

Tactic:
obtain ⟨j, h⟩ := exists_isIso_of_functor_from_monoOver (F y) hXκ _
      (colimit.isColimit (kernel (g y))) (f y) (fun j ↦ by simpa using! hf y j)
      (epi_f hc hy)

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
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
this : IsFiltered J
j : Under j₀
h : IsIso ((F y).obj j).obj.hom
⊢ ∃ j φ, y ≫ Y.map φ = 0
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
j : ι
⊢ (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).inj j ≫
      {
        hom :=
          ⋯.extend
            {
              app := fun Y ↦
                ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
              naturality := ⋯ } } =
    s.inj j

Tactic:
ext : 1

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
j : ι
⊢ ((Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).inj j ≫
        {
          hom :=
            ⋯.extend
              {
                app := fun Y ↦
                  ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
                naturality := ⋯ } }).hom =
    (s.inj j).hom