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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f₁ : a ⟶ c
u₁ : c ⟶ a
f₂ : b ⟶ d
u₂ : d ⟶ b
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : f₁ ⊣ u₁
adj₄ : f₂ ⊣ u₂
α : f₁ ≫ l₂ ⟶ l₁ ≫ f₂
⊢ (mateEquiv adj₄ adj₃) ((mateEquiv adj₁ adj₂) α) = (conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)) α

Tactic:
simp only [conjugateEquiv_apply, mateEquiv_apply']
  dsimp [Adjunction.comp]
  bicategory

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ✝ : M ⟶ N
U V : X.Opens
R S : CommRingCat
φ : R ⟶ S
⊢ sheafCompose (Opens.grothendieckTopology ↥(Spec S))
        (ModuleCat.restrictScalars (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))) ⋙
      TopCat.Sheaf.pushforward (ModuleCat ↑Γ(Spec R, ⊤)) (Spec.map φ).base ⋙
        sheafCompose (Opens.grothendieckTopology ↥(Spec R))
          (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso R).inv)) ≅
    sheafCompose (Opens.grothendieckTopology ↥(Spec S))
        (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso S).inv)) ⋙
      TopCat.Sheaf.pushforward (ModuleCat ↑S) (Spec.map φ).base ⋙
        sheafCompose (Opens.grothendieckTopology ↥(Spec R)) (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))

Tactic:
by
  refine NatIso.ofComponents (fun M ↦ ObjectProperty.isoMk _ ?_) ?_
  · refine NatIso.ofComponents (fun U ↦ ?_) ?_
    · refine (ModuleCat.restrictScalarsComp'App _ _ _ ?_ _).symm ≪≫
        (ModuleCat.restrictScalarsComp φ.hom ((Scheme.ΓSpecIso S).inv).hom).app _
      rw [← CommRingCat.hom_comp, Scheme.ΓSpecIso_inv_naturality, CommRingCat.hom_comp]
    · cat_disch
  · cat_disch

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✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
⊢ Away 𝒜 f →+* Away 𝒜 x

Tactic:
let e := RingEquiv.ofLeftInverse (f := algebraMap (Away 𝒜 x) (Localization.Away x))
    (h := (val_injective _).hasLeftInverse.choose_spec)
  refine RingHom.comp (e.symm.toRingHom.comp (Subring.inclusion ?_))
    (awayMapAux 𝒜 (f := f) ⟨_, hx⟩).rangeRestrict
  exact range_awayMapAux_subset 𝒜 hg hx

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

Goal state before:
pp: case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
⊢ fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r ≤ X.basicOpen (f r)

pp: case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
⊢ X.basicOpen (f r) ≤ fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r

Tactic:
· intro x hx
    obtain ⟨i, x, rfl⟩ := (openCoverOfMapIrrelevantEqTop 𝒜 f hf).exists_eq x
    rw [← SetLike.mem_coe] at hx -- TODO : mem version of TopologicalSpace.Opens.map_coe
    simp only [TopologicalSpace.Opens.map_coe, Set.mem_preimage, SetLike.mem_coe,
      ← Scheme.Hom.comp_apply, fromOfGlobalSections, Scheme.Cover.ι_glueMorphisms] at hx
    simp only [openCoverOfMapIrrelevantEqTop,
      toBasicOpenOfGlobalSections, Scheme.isoOfEq_inv, Category.assoc, basicOpenIsoSpec_inv_ι] at hx
    simp only [Scheme.Hom.comp_base, Scheme.homOfLE_base, homOfLE_leOfHom, TopCat.hom_comp,
      ContinuousMap.comp_assoc, ContinuousMap.comp_apply, morphismRestrict_base,
      TopologicalSpace.Opens.carrier_eq_coe] at hx
    rw [← SetLike.mem_coe, ← Set.mem_preimage, ← TopologicalSpace.Opens.map_coe,
      Proj.awayι_preimage_basicOpen (𝒜 := 𝒜) i.2.2.2 i.2.2.1 hr hn,
      ← Set.mem_preimage, ← TopologicalSpace.Opens.map_coe, ← Function.Injective.mem_set_image
      (Spec.map (CommRingCat.ofHom (algebraMap Γ(X, ⊤) _))).isOpenEmbedding.injective,
      ← Scheme.Hom.comp_apply, basicOpenIsoSpecAway, IsOpenImmersion.isoOfRangeEq_hom_fac] at hx
    rw [← SetLike.mem_coe, ← Scheme.toSpecΓ_preimage_basicOpen, TopologicalSpace.Opens.map_coe,
        Set.mem_preimage]
    refine Set.mem_of_subset_of_mem (Set.image_subset_iff.mpr ?_) hx
    change PrimeSpectrum.basicOpen _ ≤ PrimeSpectrum.basicOpen _
    simp only [CommRingCat.ofHom_comp, CommRingCat.hom_comp, CommRingCat.hom_ofHom,
      RingHom.coe_comp, Function.comp_apply, HomogeneousLocalization.algebraMap_apply,
      HomogeneousLocalization.Away.val_mk, Localization.mk_eq_mk', IsLocalization.map_mk', map_pow,
      PrimeSpectrum.basicOpen_le_basicOpen_iff, IsLocalization.mk'_mem_iff]
    exact Ideal.pow_mem_of_mem _ (Ideal.le_radical (Ideal.mem_span_singleton_self _)) _ i.2.2.1

Goal state after:
case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
⊢ X.basicOpen (f r) ≤ fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r
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) := ⋯
⊢ ∀ (x : ↥(Submonoid.powers (unop f))),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).obj g)))
        ↑x)

Tactic:
rw [Subtype.forall]
          change Submonoid.powers _ ≤ (IsUnit.submonoid _).comap _
          simp only [Submonoid.powers_le, Submonoid.mem_comap, IsUnit.mem_submonoid_iff]
          obtain ⟨n, a, e⟩ : ∃ n, f.unop ∣ g.unop ^ n := by
            simpa only [Ideal.mem_radical_iff, Ideal.mem_span_singleton] using
              (basicOpen_le_basicOpen_iff _ _).mp (i.1.hom.le)
          refine ((Commute.isUnit_mul_iff (b := algebraMap R _ a) (.map (.all _ _) _)).mp ?_).1
          rw [← map_mul, ← e, map_pow]
          exact (M.isUnit_algebraMap_end_of_le_basicOpen g.unop le_rfl).pow n

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
⊢ HomogeneousLocalization.mk { deg := m * nx, num := ⟨(proj 𝒜 nx) x ^ m, ⋯⟩, den := ⟨f ^ nx, ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal ∨
    HomogeneousLocalization.mk { deg := m * ny, num := ⟨(proj 𝒜 ny) y ^ m, ⋯⟩, den := ⟨f ^ ny, ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal

Tactic:
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']

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

Goal state before:
pp: case h₁
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 := ⋯
a : ℕ
ai : ↥s → ℕ
hai : ∑ i, ai i • dx i = a • d
hai' : ∀ (i : ↥s), ai i ≤ d
x : ↥s
a✝ : x ∈ Finset.univ
⊢ ai x ≤ d

Tactic:
exact hai' _

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

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
n : ι → ℕ
t' : (i : ι) → ↑Γ(M, basicOpen (g i))
ht' : ∀ (i : ι), f ^ n i • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t' i)
⊢ ∃ N t, ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)

Tactic:
have (i : ι) : n i ≤ ⨆ i, n i := le_ciSup (Finite.bddAbove_range _) _

Goal state after:
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
n : ι → ℕ
t' : (i : ι) → ↑Γ(M, basicOpen (g i))
ht' : ∀ (i : ι), f ^ n i • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t' i)
this : ∀ (i : ι), n i ≤ ⨆ i, n i
⊢ ∃ N t, ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
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 : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk y) =
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk z)
⊢ ∃ i, ∃ c ∈ 𝒜 i, c ∉ (↑x).asHomogeneousIdeal ∧ c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)

Tactic:
apply_fun HomogeneousLocalization.val at e
      simp only [RingHom.algebraMap_toAlgebra, map_mk, GradedRingHom.id_apply, val_mk, mk_eq_mk',
        IsLocalization.mk'_eq_iff_eq] at e
      obtain ⟨⟨c, hcx⟩, hc⟩ := IsLocalization.exists_of_eq (M := x.1.1.toIdeal.primeCompl) e
      obtain ⟨i, hi⟩ := not_forall.mp ((x.1.1.isHomogeneous.mem_iff _).not.mp hcx)
      refine ⟨i, _, (decompose 𝒜 c i).2, hi, ?_⟩
      apply_fun fun x ↦ (decompose 𝒜 x (i + z.deg + y.deg)).1 at hc
      conv_rhs at hc => rw [add_right_comm]
      rwa [← mul_assoc, coe_decompose_mul_add_of_right_mem, coe_decompose_mul_add_of_right_mem,
        ← mul_assoc, coe_decompose_mul_add_of_right_mem, coe_decompose_mul_add_of_right_mem,
        mul_assoc, mul_assoc] at hc
      exacts [y.den.2, z.num.2, z.den.2, y.num.2]

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
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
𝒰 : Cover (precoverage P) ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ T.arrows
Y : Over S
i : 𝒰.I₀
⊢ Q (𝒰.X i ↘ S)

Tactic:
← comp_over (𝒰.f i) S

Goal state after:
P Q : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
𝒰 : Cover (precoverage P) ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ T.arrows
Y : Over S
i : 𝒰.I₀
⊢ Q (𝒰.f i ≫ ((MorphismProperty.Over.forget Q ⊤ S).obj X).left ↘ S)
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₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this : IsClosedImmersion g
⊢ l₁ = l₂

Tactic:
have hZ : IsAffine Z := by
    rw [@HasAffineProperty.iff_of_isAffine @IsClosedImmersion] at this
    exact this.left

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₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this : IsClosedImmersion g
hZ : IsAffine Z
⊢ l₁ = l₂
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case h₁
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₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := ⋯
g : Z ⟶ Spec (CommRingCat.of S.R) := ⋯
this : IsClosedImmersion g
hZ : IsAffine Z
⊢ (S.i₁ ≫ pullback.diagonal f) ≫ pullback.snd f f =
    (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ pullback.lift l₁ l₂ h) ≫ pullback.snd f f

Tactic:
· simpa using hl₂.symm

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

Goal state before:
pp: case hR
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
this : F.IsCoverDense J
S : Sieve W := ⋯
T : Sieve W := ⋯
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ W⦄ (H : (Sieve.coverByImage F W).arrows f),
    Sieve.pullback (Nonempty.some H).lift
        (Sieve.functorPushforward F
          (F.imageSieve ((Nonempty.some H).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some H).map ≫ p₂))) ∈
      J Y

Tactic:
intro Y f hf
      apply J.pullback_stable
      rw [Functor.functorPushforward_mem_iff J₀]
      apply J₀.intersection_covering
      all_goals apply IsDenseSubsite.imageSieve_mem J₀ J

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
inst✝ : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
x : Φ.fiber.obj X
⊢ (ConcreteCategory.hom (Φ.presheafFiber.map (shrinkYoneda.{w, v, u}.map f)))
      ((ConcreteCategory.hom (Φ.shrinkYonedaCompPresheafFiberIso.inv.app X)) x) =
    (ConcreteCategory.hom (Φ.toPresheafFiber X x (shrinkYoneda.{w, v, u}.obj Y))) (shrinkYonedaObjObjEquiv.symm f)

Tactic:
by
  rw [shrinkYonedaCompPresheafFiberIso_inv_app_toPresheafFiber]
  refine (Φ.toPresheafFiber_naturality_apply (shrinkYoneda.{w}.map f) _ x
    (shrinkYonedaObjObjEquiv.symm (𝟙 X))).trans (congr_arg _ ?_)
  simpa using shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm.{w} (𝟙 _) f

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

Goal state before:
pp: case mp
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 : Cᵒᵖ ⥤ A
inst✝¹ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝ : LocallySmall.{w, v, u} C
X : C
x : Φ.fiber.obj X
z₁ z₂ : ToType (P.obj (op X))
⊢ (∃ j f,
      (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f)) z₁ =
        (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f)) z₂) →
    ∃ Y f y,
      (ConcreteCategory.hom (Φ.fiber.map f)) y = x ∧
        (ConcreteCategory.hom (P.map f.op)) z₁ = (ConcreteCategory.hom (P.map f.op)) z₂

Tactic:
rintro ⟨⟨Y, y⟩, ⟨f, hf⟩, hf'⟩

Goal state after:
case mp
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 : Cᵒᵖ ⥤ A
inst✝¹ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝ : LocallySmall.{w, v, u} C
X : C
x : Φ.fiber.obj X
z₁ z₂ : ToType (P.obj (op X))
Y : C
y : Φ.fiber.obj Y
f : (unop (op ⟨Y, y⟩)).fst ⟶ (unop (op ⟨X, x⟩)).fst
hf : (ConcreteCategory.hom (Φ.fiber.map f)) (unop (op ⟨Y, y⟩)).snd = (unop (op ⟨X, x⟩)).snd
hf' :
  (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map (op ⟨f, hf⟩))) z₁ =
    (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map (op ⟨f, hf⟩))) z₂
⊢ ∃ Y f y,
    (ConcreteCategory.hom (Φ.fiber.map f)) y = x ∧
      (ConcreteCategory.hom (P.map f.op)) z₁ = (ConcreteCategory.hom (P.map f.op)) z₂
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)
a : S.Arrow
i : (data a.Y).toOneHypercover.multicospanShape.L
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).toPreOneHypercover.I₀
c : F.obj X₀ ⟶ (data X).toPreOneHypercover.X j
fac₁ : c ≫ (data X).toPreOneHypercover.f j = F.map b ≫ (data a.Y).f i ≫ a.f
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨F.imageSieve c, ⋯⟩),
    (((lift hG₀ hG s ≫ G.map a.f.op) ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫
          (F.op ⋙ G).map { Y := X₀, f := b, hf := ⋯ }.f.op) ≫
        (F.op ⋙ G).map I.f.op =
      ((s.ι a ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map { Y := X₀, f := b, hf := ⋯ }.f.op) ≫
        (F.op ⋙ G).map I.f.op

Tactic:
rintro ⟨Y₀, d, e, 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
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)
a : S.Arrow
i : (data a.Y).toOneHypercover.multicospanShape.L
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).toPreOneHypercover.I₀
c : F.obj X₀ ⟶ (data X).toPreOneHypercover.X j
fac₁ : c ≫ (data X).toPreOneHypercover.f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
⊢ (((lift hG₀ hG s ≫ G.map a.f.op) ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫
        (F.op ⋙ G).map { Y := X₀, f := b, hf := ⋯ }.f.op) ≫
      (F.op ⋙ G).map { Y := Y₀, f := d, hf := ⋯ }.f.op =
    ((s.ι a ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map { Y := X₀, f := b, hf := ⋯ }.f.op) ≫
      (F.op ⋙ G).map { Y := Y₀, f := d, hf := ⋯ }.f.op
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
X : C
E : PreZeroHypercover X
⊢ E.presieve₀ ∈ P.precoverage.coverings X ↔ P.property E

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ .mk _ h⟩
  rw [PreZeroHypercoverFamily.mem_precoverage_iff] at h
  obtain ⟨F, h, heq⟩ := h
  rw [P.iff_shrink] at h ⊢
  rwa [PreZeroHypercover.shrink_eq_shrink_of_presieve₀_eq_presieve₀ heq]

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

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

Tactic:
by
    obtain ⟨E, rfl⟩ := R.exists_eq_preZeroHypercover
    obtain ⟨F, rfl⟩ := S.exists_eq_preZeroHypercover
    rw [← PreZeroHypercover.presieve₀_sum]
    rw [PreZeroHypercover.presieve₀_mem_precoverage_iff] at hR hS ⊢
    exact h hR hS

Goal state after: