mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
⊢ f.range ≤ Ideal.map (algebraMap R S) I

Tactic:
rintro - ⟨x, rfl⟩
      induction x with
      | zero => simp
      | add _ _ _ _ => simp_all [Ideal.add_mem]
      | tmul s x =>
        have : f (s ⊗ₜ[R] x) = s • f (1 ⊗ₜ x) := by simp [f]
        rw [this]
        apply Ideal.mul_mem_left
        simpa [f, Algebra.smul_def] using Ideal.mem_map_of_mem _ x.2

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : Adj B
α β : a ⟶ b
el : α.l ≅ β.l
er : β.r ≅ α.r
h : (conjugateEquiv β.adj α.adj) el.hom = er.hom
⊢ (conjugateEquiv α.adj β.adj) el.inv ≫ er.hom = 𝟙 α.r

Tactic:
← h,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : Adj B
α β : a ⟶ b
el : α.l ≅ β.l
er : β.r ≅ α.r
h : (conjugateEquiv β.adj α.adj) el.hom = er.hom
⊢ (conjugateEquiv α.adj β.adj) el.inv ≫ (conjugateEquiv β.adj α.adj) el.hom = 𝟙 α.r
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
tfae_1_to_2 : Function.Surjective ⇑(algebraMap R S) → Function.Bijective ⇑(LinearMap.mul' R S)
H : Function.Bijective ⇑(LinearMap.mul' R S)
p : PrimeSpectrum R
h : rankAtStalk (S ⊗[R] S) p = rankAtStalk S p ^ 2
hc : 1 < rankAtStalk S p
⊢ rankAtStalk S p ^ (Nat.succ 0).succ = rankAtStalk S p

Tactic:
← h,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
tfae_1_to_2 : Function.Surjective ⇑(algebraMap R S) → Function.Bijective ⇑(LinearMap.mul' R S)
H : Function.Bijective ⇑(LinearMap.mul' R S)
p : PrimeSpectrum R
h : rankAtStalk (S ⊗[R] S) p = rankAtStalk S p ^ 2
hc : 1 < rankAtStalk S p
⊢ rankAtStalk (S ⊗[R] S) p = rankAtStalk S p
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X S Y : Scheme
f : X ⟶ Y
g : Y ⟶ S
inst✝² : IsIso f
inst✝¹ : Flat g
inst✝ : IsFinite g
⊢ finrank (f ≫ g) = finrank g

Tactic:
by
  ext z
  let e : pullback (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z)) ≅
      pullback g (S.affineOpenCover.f (S.affineOpenCover.idx z)) :=
    (pullbackRightPullbackFstIso g (S.affineOpenCover.f (S.affineOpenCover.idx z)) f).symm ≪≫
      asIso (pullback.snd f (pullback.fst g (S.affineOpenCover.f _)))
  have : e.hom ≫ pullback.snd _ _ = pullback.snd _ _ := by simp [e]
  rw [finrank, finrank, ← this, IsAffine.finrank_comp_left_of_isIso]

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, IsOpen U ∧ g x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f (g x)

Tactic:
obtain ⟨U, hU, hxU, H⟩ := this (pullback.snd f g) ⟨_, rfl⟩ x

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
⊢ ∃ U, IsOpen U ∧ g x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f (g x)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ zeroLocus 𝒜 ↑(vanishingIdeal t) = closure t

Tactic:
by
  apply Set.Subset.antisymm
  · rintro x hx t' ⟨ht', ht⟩
    obtain ⟨fs, rfl⟩ : ∃ s, t' = zeroLocus 𝒜 s := by rwa [isClosed_iff_zeroLocus] at ht'
    rw [subset_zeroLocus_iff_subset_vanishingIdeal] at ht
    exact Set.Subset.trans ht hx
  · rw [(isClosed_zeroLocus _ _).closure_subset_iff]
    exact subset_zeroLocus_vanishingIdeal 𝒜 t

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
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx :
  (Scheme.Opens.ι (PrimeSpectrum.basicOpen (f i.snd.fst)))
      ((↑(PrimeSpectrum.basicOpen (f i.snd.fst))).restrictPreimage (⇑X.toSpecΓ)
        ((TopCat.Hom.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE ⋯))) x)) ∈
    ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f i.snd.fst))))) ''
      ↑((TopologicalSpace.Opens.map
              (Spec.map
                  (CommRingCat.ofHom
                    ((IsLocalization.map (Localization.Away (f i.snd.fst)) f ⋯).comp
                      (algebraMap (Away 𝒜 i.snd.fst) (Localization.Away i.snd.fst))))).base).obj
          (PrimeSpectrum.basicOpen (Away.isLocalizationElem ⋯ hr)))
⊢ ↑((TopologicalSpace.Opens.map
            (Spec.map
                (CommRingCat.ofHom
                  ((IsLocalization.map (Localization.Away (f i.snd.fst)) f ⋯).comp
                    (algebraMap (Away 𝒜 i.snd.fst) (Localization.Away i.snd.fst))))).base).obj
        (PrimeSpectrum.basicOpen (Away.isLocalizationElem ⋯ hr))) ⊆
    ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f i.snd.fst))))) ⁻¹'
      ↑(PrimeSpectrum.basicOpen (f r))

Tactic:
change PrimeSpectrum.basicOpen _ ≤ PrimeSpectrum.basicOpen _

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
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx :
  (Scheme.Opens.ι (PrimeSpectrum.basicOpen (f i.snd.fst)))
      ((↑(PrimeSpectrum.basicOpen (f i.snd.fst))).restrictPreimage (⇑X.toSpecΓ)
        ((TopCat.Hom.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE ⋯))) x)) ∈
    ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f i.snd.fst))))) ''
      ↑((TopologicalSpace.Opens.map
              (Spec.map
                  (CommRingCat.ofHom
                    ((IsLocalization.map (Localization.Away (f i.snd.fst)) f ⋯).comp
                      (algebraMap (Away 𝒜 i.snd.fst) (Localization.Away i.snd.fst))))).base).obj
          (PrimeSpectrum.basicOpen (Away.isLocalizationElem ⋯ hr)))
⊢ PrimeSpectrum.basicOpen
      ((CommRingCat.Hom.hom
          (CommRingCat.ofHom
            ((IsLocalization.map (Localization.Away (f i.snd.fst)) f ⋯).comp
              (algebraMap (Away 𝒜 i.snd.fst) (Localization.Away i.snd.fst)))))
        (Away.isLocalizationElem ⋯ hr)) ≤
    PrimeSpectrum.basicOpen
      ((CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f i.snd.fst))))) (f r))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
⊢ ∃ 𝒰, ∀ (i : 𝒰.I₀), Nonempty (SheafOfModules.Presentation (M.restrict (𝒰.f i)))

Tactic:
obtain ⟨ι, U, pres, hU, hU'⟩ := M.exists_isOpenCover_presentation

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 : 𝒰.I₀), Nonempty (SheafOfModules.Presentation (M.restrict (𝒰.f 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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x : ↑↑(Proj.restrict ⋯).toPresheafedSpace
⊢ FromSpec.toFun f_deg hm ((ConcreteCategory.hom (toSpec 𝒜 f)) x) = x

Tactic:
refine Subtype.ext <| ProjectiveSpectrum.ext <| HomogeneousIdeal.ext' ?_
  intro i z hzi
  refine (FromSpec.mem_carrier_iff_of_mem f_deg hm _ _ hzi).trans ?_
  exact (ToSpec.mk_mem_carrier _ _).trans (x.1.2.pow_mem_iff_mem m hm)

Goal state after:
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.fst f f =
    (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ pullback.lift l₁ l₂ h) ≫ pullback.fst f f

Tactic:
simpa using hl₁.symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case right
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
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))

Tactic:
· rw [@HasAffineProperty.iff_of_isAffine @IsClosedImmersion] at this
    exact this.right

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

Goal state before:
pp: case h.h
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
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
i : ι
⊢ (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) ((f ^ ⨆ i, n i) • t) =
    (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) 0

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

Goal state after:
case h.h
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
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
i : ι
this : n i ≤ ⨆ i, n i
⊢ (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) ((f ^ ⨆ i, n i) • t) =
    (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) 0
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case refine_1
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 :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
hS : S ∈ J W
hT : T ∈ J W
U V : C
a : U ⟶ V
b : V ⟶ W
hb : S.arrows b
str : Presieve.FunctorPushforwardStructure F
  (F.imageSieve ((Nonempty.some ⋯).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some ⋯).map ≫ p₂)).arrows
  ((Presieve.bind.bindStruct hb).g ≫ (Nonempty.some ⋯).lift) :=
  Presieve.getFunctorPushforwardStructure ⋯
W₀ : C₀
c : W₀ ⟶ (Presieve.getFunctorPushforwardStructure ⋯).preobj
d : U ⟶ F.obj W₀
fac : a ≫ (Presieve.getFunctorPushforwardStructure ⋯).lift = d ≫ F.map c
j : data.I₁ i₁ i₂
e : W₀ ⟶ data.Y j
h₁ : c ≫ Exists.choose ⋯ = e ≫ data.p₁ j
h₂ : c ≫ Exists.choose ⋯ = e ≫ data.p₂ j
⊢ a ≫ b ≫ p₁ = d ≫ F.map (c ≫ Exists.choose ⋯)

Tactic:
F.map_comp,

Goal state after:
case refine_1
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 :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
hS : S ∈ J W
hT : T ∈ J W
U V : C
a : U ⟶ V
b : V ⟶ W
hb : S.arrows b
str : Presieve.FunctorPushforwardStructure F
  (F.imageSieve ((Nonempty.some ⋯).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some ⋯).map ≫ p₂)).arrows
  ((Presieve.bind.bindStruct hb).g ≫ (Nonempty.some ⋯).lift) :=
  Presieve.getFunctorPushforwardStructure ⋯
W₀ : C₀
c : W₀ ⟶ (Presieve.getFunctorPushforwardStructure ⋯).preobj
d : U ⟶ F.obj W₀
fac : a ≫ (Presieve.getFunctorPushforwardStructure ⋯).lift = d ≫ F.map c
j : data.I₁ i₁ i₂
e : W₀ ⟶ data.Y j
h₁ : c ≫ Exists.choose ⋯ = e ≫ data.p₁ j
h₂ : c ≫ Exists.choose ⋯ = e ≫ data.p₂ j
⊢ a ≫ b ≫ p₁ = d ≫ F.map c ≫ F.map (Exists.choose ⋯)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case refine_2
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 :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
hS : S ∈ J W
hT : T ∈ J W
U V : C
a : U ⟶ V
b : V ⟶ W
hb : S.arrows b
str : Presieve.FunctorPushforwardStructure F
  (F.imageSieve ((Nonempty.some ⋯).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some ⋯).map ≫ p₂)).arrows
  ((Presieve.bind.bindStruct hb).g ≫ (Nonempty.some ⋯).lift) :=
  Presieve.getFunctorPushforwardStructure ⋯
W₀ : C₀
c : W₀ ⟶ (Presieve.getFunctorPushforwardStructure ⋯).preobj
d : U ⟶ F.obj W₀
fac : a ≫ (Presieve.getFunctorPushforwardStructure ⋯).lift = d ≫ F.map c
j : data.I₁ i₁ i₂
e : W₀ ⟶ data.Y j
h₁ : c ≫ Exists.choose ⋯ = e ≫ data.p₁ j
h₂ : c ≫ Exists.choose ⋯ = e ≫ data.p₂ j
⊢ a ≫ b ≫ p₂ = d ≫ F.map (c ≫ Exists.choose ⋯)

Tactic:
F.map_comp,

Goal state after:
case refine_2
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 :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
hS : S ∈ J W
hT : T ∈ J W
U V : C
a : U ⟶ V
b : V ⟶ W
hb : S.arrows b
str : Presieve.FunctorPushforwardStructure F
  (F.imageSieve ((Nonempty.some ⋯).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some ⋯).map ≫ p₂)).arrows
  ((Presieve.bind.bindStruct hb).g ≫ (Nonempty.some ⋯).lift) :=
  Presieve.getFunctorPushforwardStructure ⋯
W₀ : C₀
c : W₀ ⟶ (Presieve.getFunctorPushforwardStructure ⋯).preobj
d : U ⟶ F.obj W₀
fac : a ≫ (Presieve.getFunctorPushforwardStructure ⋯).lift = d ≫ F.map c
j : data.I₁ i₁ i₂
e : W₀ ⟶ data.Y j
h₁ : c ≫ Exists.choose ⋯ = e ≫ data.p₁ j
h₂ : c ≫ Exists.choose ⋯ = e ≫ data.p₂ j
⊢ a ≫ b ≫ p₂ = d ≫ F.map c ≫ F.map (Exists.choose ⋯)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
⊢ Aux M ⊤

Tactic:
obtain ⟨ι, U, pres, hU, hU'⟩ := M.exists_isOpenCover_presentation

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)
⊢ Aux M ⊤
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 ↔ L.essImage F

Tactic:
rw [essImage_eq_of_natIso (adj.leftAdjointUniq (constantSheafAdj J D hT))]
  exact ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨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 : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
⊢ F.map b₁ ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀

Tactic:
rw [w₁, w₂, assoc, assoc, h₁.fac, h₂.fac]

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
⊢ EffectiveEpi f → (Presieve.singleton f).EffectiveEpimorphic

Tactic:
rintro ⟨h⟩

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ (Presieve.singleton f).EffectiveEpimorphic
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
⊢ EffectiveEpiFamily X π → (Presieve.ofArrows X π).EffectiveEpimorphic

Tactic:
rintro ⟨h⟩

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (EffectiveEpiFamilyStruct X π)
⊢ (Presieve.ofArrows X π).EffectiveEpimorphic
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ S.g.app j ≫ colimit.ι S.X₃ j = c₂.ι.app j ≫ g ≫ (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)).hom

Tactic:
reassoc_of% (hg j),

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ S.g.app j ≫ colimit.ι S.X₃ j = S.g.app j ≫ c₃.ι.app j ≫ (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)).hom
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

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
F : J ⥤ MonoOver X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this✝ : IsFiltered J
this : Mono f
h : ⨆ j, Subobject.mk (F.obj j).obj.hom = ⊤
s : J → Subobject X := fun j ↦ Subobject.mk (F.obj j).obj.hom
h' : Function.Surjective fun j ↦ ⟨s j, ⋯⟩
σ : { x // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun j ↦ ⟨s j, ⋯⟩
hs : HasCardinalLT (↑(Set.range s)) κ
⊢ ⊤ ≤ Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj.hom

Tactic:
← h,

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
F : J ⥤ MonoOver X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this✝ : IsFiltered J
this : Mono f
h : ⨆ j, Subobject.mk (F.obj j).obj.hom = ⊤
s : J → Subobject X := fun j ↦ Subobject.mk (F.obj j).obj.hom
h' : Function.Surjective fun j ↦ ⟨s j, ⋯⟩
σ : { x // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun j ↦ ⟨s j, ⋯⟩
hs : HasCardinalLT (↑(Set.range s)) κ
⊢ ⨆ j, Subobject.mk (F.obj j).obj.hom ≤ Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj.hom
Module: Mathlib.Order.Interval.Set.Final

Goal state before:
pp: J : Type u
inst✝ : LinearOrder J
j : J
⊢ ⋯.functor.Final

Tactic:
rw [Monotone.final_functor_iff]
  intro k
  exact ⟨⟨max j k, le_max_left _ _⟩, le_max_right _ _⟩

Goal state after: