mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
⊢ rightZigzag η.hom ε.hom = (ρ_ g).hom ≫ (λ_ g).inv

Tactic:
rw [← cancel_epi (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv)]

Goal state after:
B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
⊢ (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ rightZigzag η.hom ε.hom =
    (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ (ρ_ g).hom ≫ (λ_ g).inv
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
⊢ rightZigzag η.hom ε.hom = (ρ_ g).hom ≫ (λ_ g).inv

Tactic:
by
  rw [← cancel_epi (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv)]
  calc
    _ = rightZigzag η.hom ε.hom ⊗≫ rightZigzag η.hom ε.hom := by bicategory
    _ = rightZigzag η.hom ε.hom := rightZigzag_idempotent_of_left_triangle _ _ h
    _ = _ := by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : IsFinite f
inst✝ : LocallyOfFinitePresentation f
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
x : ↥(Spec R)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f],
    (∃ R, Y = Spec R) → ∀ (x : ↥Y), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f x
U : Set ↥(Spec R)
hU : IsOpen U
hxU : x ∈ U
H : ∀ x' ∈ U, finrank (pullback.snd f g) x' = finrank (pullback.snd f g) x
y' : ↥(Spec R)
hyU : y' ∈ U
⊢ finrank f (g y') = finrank f (g x)

Tactic:
← finrank_pullback_snd _ g,

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : IsFinite f
inst✝ : LocallyOfFinitePresentation f
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
x : ↥(Spec R)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f],
    (∃ R, Y = Spec R) → ∀ (x : ↥Y), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f x
U : Set ↥(Spec R)
hU : IsOpen U
hxU : x ∈ U
H : ∀ x' ∈ U, finrank (pullback.snd f g) x' = finrank (pullback.snd f g) x
y' : ↥(Spec R)
hyU : y' ∈ U
⊢ finrank (pullback.snd f g) y' = finrank f (g x)
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
f g : ↑X.functionField
hf : f ≠ 0
hg : g ≠ 0
⊢ ord (f * g) x = ord f x + ord g x

Tactic:
by_cases! hx : coheight x ≠ 1

Goal state after:
case pos
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
f g : ↑X.functionField
hf : f ≠ 0
hg : g ≠ 0
hx : coheight x ≠ 1
⊢ ord (f * g) x = ord f x + ord g x

case neg
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
f g : ↑X.functionField
hf : f ≠ 0
hg : g ≠ 0
hx : coheight x = 1
⊢ ord (f * g) x = ord f x + ord g x
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx' : x ∈ U
⊢ ord ((ConcreteCategory.hom (X.germToFunctionField U)) f) x = 0

Tactic:
by_cases! hx : coheight x ≠ 1

Goal state after:
case pos
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx' : x ∈ U
hx : coheight x ≠ 1
⊢ ord ((ConcreteCategory.hom (X.germToFunctionField U)) f) x = 0

case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx' : x ∈ U
hx : coheight x = 1
⊢ ord ((ConcreteCategory.hom (X.germToFunctionField U)) f) x = 0
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : ¬f = 0
hg : ¬g = 0
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x

Tactic:
by_cases! hx : coheight x ≠ 1

Goal state after:
case pos
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : ¬f = 0
hg : ¬g = 0
hx : coheight x ≠ 1
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x

case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : ¬f = 0
hg : ¬g = 0
hx : coheight x = 1
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
inst✝ : Nonempty ↥↑U
hxU : x ∈ U
a : ↑Γ(X, U)
ha : a ≠ 0
f : ↑X.functionField
⊢ ord f x ≤ ord (a • f) x

Tactic:
by_cases! hx : coheight x ≠ 1

Goal state after:
case pos
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
inst✝ : Nonempty ↥↑U
hxU : x ∈ U
a : ↑Γ(X, U)
ha : a ≠ 0
f : ↑X.functionField
hx : coheight x ≠ 1
⊢ ord f x ≤ ord (a • f) x

case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
inst✝ : Nonempty ↥↑U
hxU : x ∈ U
a : ↑Γ(X, U)
ha : a ≠ 0
f : ↑X.functionField
hx : coheight x = 1
⊢ ord f x ≤ ord (a • f) x
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₁
⊢ (conjugateEquiv adj₁ adj₁) (𝟙 l₁) = 𝟙 r₁

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

Goal state after:
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 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
hb : (isLocallyFraction 𝒜).pred b
x : ↥(unop U)
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ unop U
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal
wa :
  ∀ (x : ↥Va),
    (fun x ↦ a (ia x)) x =
      HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ unop U
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal
wb :
  ∀ (x : ↥Vb),
    (fun x ↦ b (ib x)) x =
      HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal 𝒜).pred fun x ↦ (a * b) (i x)

Tactic:
refine
    ⟨Va ⊓ Vb, ⟨ma, mb⟩, Opens.infLELeft _ _ ≫ ia, ja + jb,
      ⟨ra * rb, SetLike.mul_mem_graded ra_mem rb_mem⟩,
      ⟨sa * sb, SetLike.mul_mem_graded sa_mem sb_mem⟩, fun y =>
      y.1.asHomogeneousIdeal.toIdeal.primeCompl.mul_mem (hwa ⟨y.1, y.2.1⟩) (hwb ⟨y.1, y.2.2⟩), ?_⟩

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
hb : (isLocallyFraction 𝒜).pred b
x : ↥(unop U)
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ unop U
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal
wa :
  ∀ (x : ↥Va),
    (fun x ↦ a (ia x)) x =
      HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ unop U
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal
wb :
  ∀ (x : ↥Vb),
    (fun x ↦ b (ib x)) x =
      HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }
⊢ ∀ (x : ↥(Va ⊓ Vb)),
    (fun x ↦ (a * b) ((Va.infLELeft Vb ≫ ia) x)) x =
      HomogeneousLocalization.mk { deg := ja + jb, num := ⟨ra * rb, ⋯⟩, den := ⟨sa * sb, ⋯⟩, den_mem := ⋯ }
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
M : Y.Modules
U V : X.Opens
hUV : Opposite.op V ⟶ Opposite.op U
⊢ (M.restrict f).presheaf.map hUV ≫ (restrictAppIso f M U).hom =
    (restrictAppIso f M V).hom ≫ M.presheaf.map (homOfLE ⋯).op

Tactic:
by
  rfl

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 : ↑(Proj.restrict ⋯).toTopCat
⊢ (Ideal.map (algebraMap A (Away f)) (↑x).asHomogeneousIdeal.toIdeal).IsPrime

Tactic:
exact IsLocalization.isPrime_of_isPrime_disjoint
    (Submonoid.powers f) _ _ inferInstance
    ((disjoint_powers_iff_notMem_of_isPrime _).mpr x.2)

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

Goal state before:
pp: R : CommRingCat
M N P : ModuleCat ↑R
f : M ⟶ N
g : N ⟶ P
⊢ tilde.map (f ≫ g) = tilde.map f ≫ tilde.map g

Tactic:
ext p x
  exact Subtype.ext (funext
    fun y ↦ DFunLike.congr_fun (IsLocalizedModule.map_comp' y.1.asIdeal.primeCompl
      (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl M)
      (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl N)
      (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl P) _ _) _)

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps

Goal state before:
pp: case mem
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst✝¹³ : Semiring A
inst✝¹² : Semiring B
inst✝¹¹ : Semiring C
inst✝¹⁰ : SetLike σ A
inst✝⁹ : SetLike τ B
inst✝⁸ : SetLike ω C
inst✝⁷ : AddSubmonoidClass σ A
inst✝⁶ : AddSubmonoidClass τ B
inst✝⁵ : AddSubmonoidClass ω C
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
b a : B
ha : a ∈ ⇑f '' ↑I.toIdeal
i : ι
⊢ ↑(((DirectSum.decompose ℬ) a) i) ∈ Ideal.map f I.toIdeal

Tactic:
| mem a ha =>

Goal state after:
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:
by
  suffices ∀ x ∉ R.toSubring, x⁻¹ ∈ R.toSubring from
    ⟨⟨R.toSubring, fun x ↦ or_iff_not_imp_left.mpr (this x)⟩, rfl⟩
  refine fun x hx ↦ mem_of_isMax_of_isIntegral hR ?_
  have hx0 : x ≠ 0 := fun e ↦ hx (e ▸ zero_mem _)
  let := invertibleOfNonzero hx0
  let S := R.toSubring[x]
  have : R.toSubring < S.toSubring := SetLike.lt_iff_le_and_exists.mpr
    ⟨fun r hr ↦ algebraMap_mem S ⟨r, hr⟩, ⟨x, self_mem_adjoin_singleton _ _, hx⟩⟩
  have ⟨p, hp, hpx⟩ := exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top x _
    (maximalIdeal.isMaximal R.toSubring).ne_top
    (top_unique <| (map_maximalIdeal_eq_top_of_isMax hR this).ge.trans le_self_add)
  have H : IsUnit p.leadingCoeff := of_not_not fun h ↦ by simpa using sub_mem h hp
  exact ⟨.C H.unit⁻¹.1 * p, by simp [Polynomial.Monic], by simpa using .inr hpx⟩

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
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]
      · apply q.2.mem_or_mem; convert! hxy (nx + ny)
        dsimp
        simp_rw [decompose_of_mem_same 𝒜 hnx, decompose_of_mem_same 𝒜 hny,
          decompose_of_mem_same 𝒜 (SetLike.GradedMonoid.toGradedMul.mul_mem hnx hny),
          mul_pow, pow_add]
        simp only [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk,
          HomogeneousLocalization.val_mul, Localization.mk_mul]
        simp only [Submonoid.mk_mul_mk, mk_eq_monoidOf_mk']
      all_goals
        intro n hn; convert q.1.zero_mem
        rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk,
          HomogeneousLocalization.val_zero]; simp_rw [proj_apply]
        convert! mk_zero (S := Submonoid.powers f) _
        rw [decompose_of_mem_ne 𝒜 _ hn.symm, zero_pow hm.ne']
        · first | exact hnx | exact hny

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

Goal state before:
pp: case mp
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ R ∈ (overPretopology P S).toGrothendieck X → ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows

Tactic:
rintro ⟨T, ⟨𝒰, h, rfl⟩, hle⟩

Goal state after:
case mp
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ R.arrows
⊢ ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ (∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows) → R ∈ (overPretopology P S).toGrothendieck X

Tactic:
rintro ⟨𝒰, h𝒰, hle⟩
    exact ⟨𝒰.toPresieveOver, ⟨𝒰, h𝒰, rfl⟩, hle⟩

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

Goal state before:
pp: case refine_1
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
x : ↥X.left
⊢ ∃ Y f y, R.arrows f ∧ P f.left ∧ f.left y = x

Tactic:
obtain ⟨y, hy⟩ := 𝒰.covers x

Goal state after:
case refine_1
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
x : ↥X.left
y : ↥(𝒰.X (𝒰.idx x))
hy : (𝒰.f (𝒰.idx x)) y = x
⊢ ∃ Y f y, R.arrows f ∧ P f.left ∧ f.left y = x
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
rid : φ (Away.isLocalizationElem ⋯ ⋯) = 0
⊢ 0 = Kmax

Tactic:
simpa [ψ, rid, Finset.prod_eq_zero_iff, (hdi _).ne'] using hi1

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Basic

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁶ : Category.{v', u'} A
inst✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
P Q : Cᵒᵖ ⥤ A
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝¹ : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst✝ : Presheaf.IsLocallyInjective J f
X : C
x : Φ.fiber.obj X
p₁ : ToType (P.obj (op X))
⊢ ∀ (p₂ : ToType (P.obj (op X))),
    (ConcreteCategory.hom (f.app (op X))) p₁ = (ConcreteCategory.hom (f.app (op X))) p₂ →
      (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₁ = (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₂

Tactic:
p₂

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁶ : Category.{v', u'} A
inst✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
P Q : Cᵒᵖ ⥤ A
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝¹ : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst✝ : Presheaf.IsLocallyInjective J f
X : C
x : Φ.fiber.obj X
p₁ p₂ : ToType (P.obj (op X))
⊢ (ConcreteCategory.hom (f.app (op X))) p₁ = (ConcreteCategory.hom (f.app (op X))) p₂ →
    (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₁ = (ConcreteCategory.hom (Φ.toPresheafFiber X x 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
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha : (↑⟨Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) ↑S), ⋯⟩).arrows a
ha₁ : (↑S).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
⊢ s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁, hf := ha₁ } =
    liftAux hG₀ s i₂ ≫ G.map (F.map (a ≫ (data X).p₂ j)).op

Tactic:
liftAux_fac _ _ _ ha₂

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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha : (↑⟨Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) ↑S), ⋯⟩).arrows a
ha₁ : (↑S).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
⊢ s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁, hf := ha₁ } =
    s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂, hf := ha₂ }
Module: Mathlib.CategoryTheory.Sites.ConstantSheaf

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
inst✝ : HasWeakSheafify J D
L : D ⥤ Sheaf J D
T : C
hT : IsTerminal T
adj : L ⊣ (sheafSections J D).obj (Opposite.op T)
F : Sheaf J D
⊢ IsConstant J F ↔ (constantSheaf J D).essImage F

Tactic:
exact ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: case refine_2
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)
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
F : (i : ι) → PreZeroHypercover (E.X i) := fun i ↦ { I₀ := σ i, X := Y i, f := g i }
i : E.I₀
⊢ (F i).presieve₀ ∈ P.precoverage.coverings (E.X i)

Tactic:
exact hg i

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

Goal state before:
pp: case refine_1
S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ (𝒰.restrictIndex (Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom 𝒰.forgetQc.toPreZeroHypercover).s₀)).presieve₀ ∈
    qcPrecoverage.coverings S

Tactic:
Scheme.presieve₀_mem_qcPrecoverage_iff

Goal state after:
case refine_1
S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ QuasiCompactCover
    (𝒰.restrictIndex (Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom 𝒰.forgetQc.toPreZeroHypercover).s₀))
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
⊢ ∃ T' π, ∃ (_ : Epi π), ∃ x₂ x₃, π ≫ x₄ = x₂ ≫ r + x₃ ≫ b

Tactic:
have := h.epi_shortComplex_g

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi ⋯.shortComplex.g
⊢ ∃ T' π, ∃ (_ : Epi π), ∃ x₂ x₃, π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
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₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
⊢ (y₁ - y₂) ≫ c.ι.app j₀ = 0

Tactic:
by rw [Preadditive.sub_comp, sub_eq_zero, hy]

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

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i i' : ↑(Set.Iic j)
hi' : i < i'
⊢ ∃ b, ↑i < b

Tactic:
exact ⟨j, lt_of_lt_of_le hi' i'.2⟩

Goal state after: