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

Goal state before:
pp: case hy
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
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)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
⊢ ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d) ∈
    Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}

Tactic:
apply prod_mem

Goal state after:
case hy
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
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)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
⊢ ∀ c ∈ Finset.univ,
    isLocalizationElem hf ⋯ ^ (ai c / d) ∈
      Algebra.adjoin ↥(𝒜 0)
        {x |
          ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case hy
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
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)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
⊢ ∀ c ∈ Finset.univ,
    isLocalizationElem hf ⋯ ^ (ai c / d) ∈
      Algebra.adjoin ↥(𝒜 0)
        {x |
          ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}

Tactic:
rintro j -

Goal state after:
case hy
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
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)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
j : ι'
⊢ isLocalizationElem hf ⋯ ^ (ai j / d) ∈
    Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case inr
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
hs' : ∀ i ∈ s, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n
dx : ↥s → ℕ
hdx : ∀ (x : ↥s), dx x ≠ 0
hxd : ∀ (x : ↥s), ↑x ∈ 𝒜 (dx x)
hd : d > 0
b : ℕ := ∑ i, dx i
s' : Set (Fin (b + 1) × (↥s → Fin (d + 1))) := {ai | ∑ i, ↑(ai.2 i) * dx i = ↑ai.1 * d}
F : ↑s' → Away 𝒜 f := fun ai ↦ Away.mk 𝒜 hf (↑(↑ai).1) (∏ i, ↑i ^ ↑((↑ai).2 i)) ⋯
⊢ {x |
      ∃ a ai,
        ∃ (hai : ∑ i, ai i • dx i = a • d) (_ : ∀ (i : ↥s), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, ↑i ^ ai i) ⋯ = x}.Finite

Tactic:
apply (Set.finite_range F).subset

Goal state after:
case inr
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
hs' : ∀ i ∈ s, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n
dx : ↥s → ℕ
hdx : ∀ (x : ↥s), dx x ≠ 0
hxd : ∀ (x : ↥s), ↑x ∈ 𝒜 (dx x)
hd : d > 0
b : ℕ := ⋯
s' : Set (Fin (b + 1) × (↥s → Fin (d + 1))) := ⋯
F : ↑s' → Away 𝒜 f := ⋯
⊢ {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dx i = a • d) (_ : ∀ (i : ↥s), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, ↑i ^ ai i) ⋯ = x} ⊆
    Set.range F
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
n : ℕ
hn : n ≠ ny
⊢ Localization.mk (↑(((decompose 𝒜) y) n) ^ m) ⟨f ^ n, ⋯⟩ = 0

Tactic:
convert! mk_zero (S := Submonoid.powers f) _

Goal state after:
case e'_4
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
n : ℕ
hn : n ≠ ny
⊢ ↑(((decompose 𝒜) y) n) ^ m = 0
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
n : ℕ
hn : n ≠ nx
⊢ Localization.mk (↑(((decompose 𝒜) x) n) ^ m) ⟨f ^ n, ⋯⟩ = 0

Tactic:
convert! mk_zero (S := Submonoid.powers f) _

Goal state after:
case e'_4
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
n : ℕ
hn : n ≠ nx
⊢ ↑(((decompose 𝒜) x) n) ^ m = 0
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
x : S
y : R
hy : (algebraMap R K) y = g x
⊢ ↑((g.rangeRestrict.comp f) y) = ↑⟨g x, ⋯⟩

Tactic:
simpa [← h] using hy

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing✝ : CommRing R
domain✝ : IsDomain R
valuationRing✝ : ValuationRing R
K : Type u
field✝ : Field K
algebra✝ : Algebra R K
isFractionRing✝ : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this✝³ : IsDomain ↑(CommRingCat.of R)
this✝² : ValuationRing ↑(CommRingCat.of R)
this✝¹ : Field ↑(CommRingCat.of K) := field✝
H : topologically (@SpecializingMap) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ : flip (fun x1 x2 ↦ x1 ⤳ x2) x (lft (closedPoint ↑(CommRingCat.of K)))
h₂ : (pullback.fst i₂ f) x = closedPoint R
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  (stalkClosedPointIso (CommRingCat.of R)).symm ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this✝ : IsLocalHom (CommRingCat.Hom.hom e.hom)
this : IsLocalHom (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K)
hbij : Function.Bijective ⇑((CommRingCat.Hom.hom β).rangeRestrict.comp (CommRingCat.Hom.hom α))
φ : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of R :=
  CommRingCat.ofHom
    ((RingEquiv.ofBijective ((CommRingCat.Hom.hom β).rangeRestrict.comp (CommRingCat.Hom.hom α))
              hbij).symm.toRingHom.comp
      (CommRingCat.Hom.hom β).rangeRestrict)
hαφ : α ≫ φ = 𝟙 (CommRingCat.of R)
hαφ' : Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫ φ = e.inv
hφβ : φ ≫ CommRingCat.ofHom (algebraMap R K) = β
⊢ Spec.map
        (CommRingCat.ofHom
          (algebraMap
            { R := R, commRing := commRing✝, domain := domain✝, valuationRing := valuationRing✝, K := K,
                field := field✝, algebra := algebra✝, isFractionRing := isFractionRing✝, i₁ := i₁, i₂ := i₂,
                commSq := ⋯ }.R
            { R := R, commRing := commRing✝, domain := domain✝, valuationRing := valuationRing✝, K := K,
                field := field✝, algebra := algebra✝, isFractionRing := isFractionRing✝, i₁ := i₁, i₂ := i₂,
                commSq := ⋯ }.K)) ≫
      Spec.map (Scheme.Hom.stalkMap (pullback.snd i₂ f) x ≫ φ) ≫ X.fromSpecStalk ((pullback.snd i₂ f) x) =
    { R := R, commRing := commRing✝, domain := domain✝, valuationRing := valuationRing✝, K := K, field := field✝,
        algebra := algebra✝, isFractionRing := isFractionRing✝, i₁ := i₁, i₂ := i₂, commSq := ⋯ }.i₁

Tactic:
simp only [← Spec.map_comp_assoc, Category.assoc, hφβ]
    simp only [Spec.map_comp, Category.assoc, Scheme.SpecMap_stalkMap_fromSpecStalk,
      Scheme.SpecMap_stalkSpecializes_fromSpecStalk_assoc, β]
    -- This next line only fires as `rw`, not `simp`:
    rw [Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc]
    simp [lft]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X✝ Y : Scheme
f : X✝ ⟶ Y
Y' X X' : Scheme
⊢ ∀ {S : Scheme} {f : Y' ⟶ S} {g : X ⟶ S} {f' : X' ⟶ X} {g' : X' ⟶ Y'},
    IsPullback f' g' g f → Existence g → Existence g'

Tactic:
Y

Goal state after:
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
Y' X X' Y : Scheme
⊢ ∀ {f : Y' ⟶ Y} {g : X ⟶ Y} {f' : X' ⟶ X} {g' : X' ⟶ Y'}, IsPullback f' g' g f → Existence g → Existence g'
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
⊢ overGrothendieckTopology P S = (overPretopology P S).toGrothendieck

Tactic:
ext X R

Goal state after:
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ R ∈ (overGrothendieckTopology P S) X ↔ R ∈ (overPretopology P S).toGrothendieck X
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: 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 Y : Q.Over ⊤ S⦄ (f : Y ⟶ X),
    ∀ S_1 ∈ {R | ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp h},
      Presieve.pullbackArrows f S_1 ∈ {R | ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp h}

Tactic:
by
    rintro Y X f _ ⟨𝒰, h, p, rfl⟩
    refine ⟨𝒰.pullbackCoverOverProp' S f.left (Q := Q) Y.prop X.prop p, inferInstance, ?_, ?_⟩
    · intro j
      apply MorphismProperty.Comma.prop
    · exact (Presieve.ofArrows_pullback f (fun i ↦ ⟨(𝒰.X i).asOver S, p i⟩)
        (fun i ↦ ⟨(𝒰.f i).asOver S, trivial, trivial⟩)).symm

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

Goal state before:
pp: P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
hPQ : P ≤ Q
⊢ smallGrothendieckTopology P S = (smallPretopology P Q).toGrothendieck

Tactic:
ext X R

Goal state after:
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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
⊢ R ∈ (smallGrothendieckTopology P S) X ↔ R ∈ (smallPretopology P Q).toGrothendieck X
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
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ R ∈ (smallPretopology P P).toGrothendieck X →
    ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows

pp: case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ (∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows) →
    R ∈ (smallPretopology P P).toGrothendieck X

Tactic:
· rintro ⟨T, ⟨𝒰, h, p, rfl⟩, hle⟩
    use 𝒰, h, p

Goal state after:
case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ (∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows) →
    R ∈ (smallPretopology P P).toGrothendieck X
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
⊢ Function.Injective ⇑(ConcreteCategory.hom (Φ.presheafFiber.map f))

Tactic:
by
  suffices ∀ (X : C) (x : Φ.fiber.obj X) (p₁ p₂ : ToType (P.obj (op X)))
      (hp : f.app _ p₁ = f.app _ p₂), Φ.toPresheafFiber X x P p₁ = Φ.toPresheafFiber X x P p₂ by
    rintro q₁ q₂ h
    obtain ⟨X, x, p₁, p₂, rfl, rfl⟩ := Φ.toPresheafFiber_jointly_surjective₂ q₁ q₂
    simp only [toPresheafFiber_naturality_apply, toPresheafFiber_eq_iff'] at h
    obtain ⟨Y, g, y, rfl, h⟩ := h
    simp only [← NatTrans.naturality_apply] at h
    simpa using this _ y _ _ h
  intro X x p₁ p₂ h
  obtain ⟨Y, g, hg, y, rfl⟩ := Φ.jointly_surjective _ (Presheaf.equalizerSieve_mem J f _ _ h) x
  simp_all [← toPresheafFiber_w_apply]

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

Goal state before:
pp: X : Scheme
⊢ ∀ ⦃Y : Scheme⦄ (f : X ⟶ Y), IsOpenImmersion f → Etale f

Tactic:
Y

Goal state after:
X Y : Scheme
⊢ ∀ (f : X ⟶ Y), IsOpenImmersion f → Etale f
Module: Mathlib.AlgebraicGeometry.Sites.Etale

Goal state before:
pp: case refine_1
X : Scheme
W : X.Etale
ι : Type u_1
Z : ι → X.Etale
f : (i : ι) → Z i ⟶ W
hf : Sieve.ofArrows Z f ∈ X.smallEtaleTopology W
U : Cover (precoverage @Etale) W.left
w✝¹ : Cover.Over X U
w✝ : ∀ (j : U.I₀), Etale (U.X j ↘ X)
hU : U.toPresieveOverProp w✝ ≤ (Sieve.ofArrows Z f).arrows
i : U.I₀
u : ↥(U.X i)
Y : X.Etale
j : ι
b : (U.X i).asOverProp X ⋯ ⟶ Z j
fac : b.left ≫ (f j).left = U.f i
⊢ ∃ i_1 y, (f i_1).left y = (U.f i) u

Tactic:
exact ⟨j, b.left u, by simp [← fac]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
ι : Type w
S : ι → A
hS : (ObjectProperty.ofObj S).IsSeparating
F G : Cᵒᵖ ⥤ A
f g : F ⟶ G
h :
  ∀ (G_1 : Cᵒᵖ ⥤ A),
    ObjectProperty.ofObj
        (fun x ↦
          match x with
          | (X, i) => freeYoneda X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
α : S i ⟶ F.obj (op X)
⊢ freeYonedaHomEquiv.symm (α ≫ f.app (op X)) = freeYonedaHomEquiv.symm (α ≫ g.app (op X))

Tactic:
simpa only [freeYonedaHomEquiv_symm_comp] using
    h _ (ObjectProperty.ofObj_apply _ ⟨X, i⟩) (freeYonedaHomEquiv.symm α)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
⊢ (fun P ↦ P.precoverage) ((fun K ↦ K.preZeroHypercoverFamily) K) = K

Tactic:
ext X R

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
X : C
R : Presieve X
⊢ R ∈ ((fun P ↦ P.precoverage) ((fun K ↦ K.preZeroHypercoverFamily) K)).coverings X ↔ R ∈ K.coverings X
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: S : Scheme
X Y : Scheme
f : X ⟶ Y
hf : IsIso f
⊢ qcCoverFamily.property (PreZeroHypercover.singleton f)

Tactic:
rw [qcCoverFamily_property, Scheme.quasiCompactCover_iff]

Goal state after:
S : Scheme
X Y : Scheme
f : X ⟶ Y
hf : IsIso f
⊢ QuasiCompactCover (PreZeroHypercover.singleton f)
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: case refine_2
S : Scheme
X : Scheme
⊢ ∀ {Y : Scheme} (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst : ∀ (i : E.I₀), HasPullback f (E.f i)],
    qcCoverFamily.property E → qcCoverFamily.property (PreZeroHypercover.pullback₁ f E)

Tactic:
Y

Goal state after:
case refine_2
S : Scheme
X Y : Scheme
⊢ ∀ (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst : ∀ (i : E.I₀), HasPullback f (E.f i)],
    qcCoverFamily.property E → qcCoverFamily.property (PreZeroHypercover.pullback₁ f E)
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: ⊢ Monotone propQCPrecoverage

Tactic:
intro P Q h
  rw [propQCPrecoverage, propQCPrecoverage]
  gcongr
  exact precoverage_mono h

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₀ W₀ : C₀
a : F.obj W₀ ⟶ F.obj X₀
i : (data (F.obj X₀)).I₀
p : F.obj W₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac : p ≫ (data (F.obj X₀)).f i = a
T₀ : C₀
b : T₀ ⟶ W₀
c : T₀ ⟶ X₀
hc : F.map c = F.map b ≫ a
⊢ (hom data G₀ X₀ ≫ IsDenseSubsite.mapPreimage J F G₀ a) ≫ G₀.obj.map b.op =
    (presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p) ≫ G₀.obj.map b.op

Tactic:
simp only [assoc, IsDenseSubsite.mapPreimage_comp_map, ← hc,
    IsDenseSubsite.mapPreimage_map]

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₀ W₀ : C₀
a : F.obj W₀ ⟶ F.obj X₀
i : (data (F.obj X₀)).I₀
p : F.obj W₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac : p ≫ (data (F.obj X₀)).f i = a
T₀ : C₀
b : T₀ ⟶ W₀
c : T₀ ⟶ X₀
hc : F.map c = F.map b ≫ a
⊢ hom data G₀ X₀ ≫ G₀.obj.map c.op = presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map b ≫ p)
Module: Mathlib.AlgebraicGeometry.Sites.Proetale

Goal state before:
pp: X : Scheme
⊢ ∀ ⦃Y : Scheme⦄ (f : X ⟶ Y), Etale f → WeaklyEtale f

Tactic:
Y

Goal state after:
X Y : Scheme
⊢ ∀ (f : X ⟶ Y), Etale f → WeaklyEtale f
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 (max v v'))
f : (uliftYoneda.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (F.obj.map g.op)) (J.uliftYonedaEquiv f) =
    (ConcreteCategory.hom (f.hom.app (op Y))) { down := g }

Tactic:
rw [uliftYonedaEquiv_naturality, uliftYonedaEquiv_comp, uliftYonedaEquiv_uliftYoneda_map]

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

Goal state before:
pp: case pos
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)
s : Cofan fun i ↦ J.yoneda.obj (X i)
Y : C
i j : ι
a : Y ⟶ X i
b : Y ⟶ X j
hab : a ≫ c.inj i = b ≫ c.inj j
h : i = j
⊢ (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b

Tactic:
subst h

Goal state after:
case pos
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)
s : Cofan fun i ↦ J.yoneda.obj (X i)
Y : C
i : ι
a b : Y ⟶ X i
hab : a ≫ c.inj i = b ≫ c.inj i
⊢ (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) b
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), transfiniteCompositions.{w, v, u} W₁ f → transfiniteCompositions.{w, v, u} W₂ f

Tactic:
Y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
⊢ ∀ (f : X ⟶ Y), transfiniteCompositions.{w, v, u} W₁ f → transfiniteCompositions.{w, v, u} W₂ f
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ F.map (homOfLE ⋯) = eqToHom ⋯ ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯

Tactic:
← homOfLE_comp (y := ⟨i₂, h₂₃.trans h₃⟩) h₁₂ h₂₃

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ F.map (homOfLE h₁₂ ≫ homOfLE h₂₃) = eqToHom ⋯ ≫ G.map (homOfLE h₁₂ ≫ homOfLE h₂₃) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case isMin
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : IsMin i
⊢ Nonempty (Φ.Iteration i)

Tactic:
obtain rfl : i = ⊥ := by simpa using hi

Goal state after:
case isMin
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
hi : IsMin ⊥
⊢ Nonempty (Φ.Iteration ⊥)