mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
hVW' : ↑W = (↑V)ᶜ
⊢ ∃ U, (toNormalization (pullback.snd f fT)) ↑v ∈ U ∧ IsIso (toNormalization (pullback.snd f fT) ∣_ U)

Tactic:
have : IsClosedImmersion V.ι := .of_isPreimmersion _ (by simp [eq_compl_comm.mp hVW', W.isOpen])

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
hVW' : ↑W = (↑V)ᶜ
this : IsClosedImmersion V.ι
⊢ ∃ U, (toNormalization (pullback.snd f fT)) ↑v ∈ U ∧ IsIso (toNormalization (pullback.snd f fT) ∣_ U)
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
I : Ideal S
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
⊢ (tensorCotangentHom R T I) 0 =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) 0, ⋯⟩

Tactic:
by simp only [map_zero]; exact (map_zero _).symm

Goal state after:
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
I : Ideal S
inst✝ : Module.Flat R T
a : S →+* T ⊗[R] S := ⋯
f : (map a I).Cotangent →ₗ[T] T ⊗[R] S ⧸ map a I ^ 2 := ⋯
g : T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2) := ⋯
hₐ : T ⊗[R] (S ⧸ I ^ 2) ≃ₐ[T] T ⊗[R] S ⧸ map a I ^ 2 := ⋯
this : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
⊢ Function.Injective ⇑g

Tactic:
· apply Module.Flat.lTensor_preserves_injective_linearMap (M := T)
      (I.cotangentToQuotientSquare.restrictScalars R)
    apply cotangentToQuotientSquare_injective

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

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv

Tactic:
calc
    _ = 𝟙 _ ⊗≫
          (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
            g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫
              adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 _ := by
      dsimp only [compUnit, compCounit]; bicategory
    _ = 𝟙 _ ⊗≫
          g₂ ◁ (rightZigzag adj₁.unit adj₁.counit) ⊗≫
            (rightZigzag adj₂.unit adj₂.counit) ▷ g₁ ⊗≫ 𝟙 _ := by
      rw [whisker_exchange]; bicategory
    _ = _ := by
      simp_rw [right_triangle]; bicategory

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
⊢ ringKrullDim R + ⊤ ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
suffices ringKrullDim (MvPolynomial σ R) = ⊤ by simp_all

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
⊢ ringKrullDim (MvPolynomial σ R) = ⊤
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝¹ : CommRing A
inst✝ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
i1 : ι
n1 : A
hn1 : n1 ∈ 𝒜 i1
d1 : A
hd1 : d1 ∈ 𝒜 i1
h1 : ↑⟨d1, hd1⟩ ∈ x
i2 : ι
n2 : A
hn2 : n2 ∈ 𝒜 i2
d2 : A
hd2 : d2 ∈ 𝒜 i2
h2 : ↑⟨d2, hd2⟩ ∈ x
hdeg : i1 = i2
hnum : n1 = n2
hden : d1 = d2
⊢ { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 } =
    { deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }

Tactic:
subst hdeg hnum hden

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝¹ : CommRing A
inst✝ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
i1 : ι
n1 : A
hn1 : n1 ∈ 𝒜 i1
d1 : A
hd1 : d1 ∈ 𝒜 i1
h1 : ↑⟨d1, hd1⟩ ∈ x
hn2 : n1 ∈ 𝒜 i1
hd2 : d1 ∈ 𝒜 i1
h2 : ↑⟨d1, hd2⟩ ∈ x
⊢ { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 } =
    { deg := i1, num := ⟨n1, hn2⟩, den := ⟨d1, hd2⟩, den_mem := h2 }
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst✝ : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ M.presheaf.germ (f ''ᵁ Opposite.unop (Opposite.op U)) (f x) ⋯ ≫ (restrictStalkNatIso f x).inv.app M =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU

Tactic:
rw [← germ_restrictStalkNatIso_hom_app f x M hxU, Category.assoc, ← NatTrans.comp_app,
    Iso.hom_inv_id]

Goal state after:
X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst✝ : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ ((restrictFunctor f).obj M).presheaf.germ U x hxU ≫
      (𝟙 (restrictFunctor f ⋙ toPresheaf X ⋙ TopCat.Presheaf.stalkFunctor Ab x)).app M =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU
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
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ HomogeneousLocalization.mk { deg := m * n, num := ⟨(proj 𝒜 n) a ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal ↔
    HomogeneousLocalization.mk { deg := m * n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal

Tactic:
· simp only [proj_apply, decompose_of_mem_same _ hn]

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

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm =
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' ?hx).hom ≫ awayι 𝒜 ?x ⋯ ⋯

pp: case x
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ A

pp: case hx
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ ?x = f * g

Tactic:
SpecMap_awayMap_awayι

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ awayι 𝒜 x ⋯ ⋯ =
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' ?hx✝).hom ≫ awayι 𝒜 ?x✝ ⋯ ⋯

case x
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ A

case hx
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ ?x✝ = f * g
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg ⋯)) ≫ awayι 𝒜 g g_deg hm' =
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ awayι 𝒜 x ⋯ ⋯

Tactic:
SpecMap_awayMap_awayι

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ awayι 𝒜 x ⋯ ⋯ =
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ awayι 𝒜 x ⋯ ⋯
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case e_a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t : A
d : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x : PrimeSpectrum.basicOpen x' ≤ PrimeSpectrum.basicOpen x
H' : f (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
⊢ (basicOpenIsoSpecAway x').inv ≫
      (Spec Γ(X, ⊤)).homOfLE hx'x ≫
        (basicOpenIsoSpecAway x).hom ≫
          Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x) f ⋯)) ≫
            Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t) (Localization.Away t))) ≫ awayι 𝒜 t hd h0d =
    Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x') f ⋯)) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 (t * s)) (Localization.Away (t * s)))) ≫
        Spec.map (CommRingCat.ofHom (awayMap 𝒜 hs ⋯)) ≫ awayι 𝒜 t hd h0d

Tactic:
basicOpenIsoSpecAway_inv_homOfLE_assoc (R := Γ(X, ⊤)) x (f s) x' (by simp [← H', H]),

Goal state after:
case e_a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t : A
d : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x : PrimeSpectrum.basicOpen x' ≤ PrimeSpectrum.basicOpen x
H' : f (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
⊢ Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight x (f s))) ≫
      (basicOpenIsoSpecAway x).inv ≫
        (basicOpenIsoSpecAway x).hom ≫
          Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x) f ⋯)) ≫
            Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t) (Localization.Away t))) ≫ awayι 𝒜 t hd h0d =
    Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x') f ⋯)) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 (t * s)) (Localization.Away (t * s)))) ≫
        Spec.map (CommRingCat.ofHom (awayMap 𝒜 hs ⋯)) ≫ awayι 𝒜 t hd h0d
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A : Type u_1
B : Type u_2
σ : Type u_4
τ : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
U : Opens (ProjectiveSpectrum 𝒜)
V : Opens (ProjectiveSpectrum ℬ)
hUV : V.carrier ⊆ ⇑(ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier
s : (x : ↥U) → AtPrime 𝒜 (↑x).asHomogeneousIdeal.toSubmodule
hs : (ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred s
⊢ (ProjectiveSpectrum.StructureSheaf.isLocallyFraction ℬ).pred (comapStructureSheafFun f hf U V hUV s)

Tactic:
by
  rintro ⟨p, hpV⟩
  rcases hs ⟨.comap f hf p, hUV hpV⟩ with ⟨W, m, iWU, i, a, b, hb, h_frac⟩
  refine ⟨W.comap (ProjectiveSpectrum.comap f hf) ⊓ V, ⟨m, hpV⟩, Opens.infLERight _ _, i,
    f.gradedAddHom i a, f.gradedAddHom i b, fun ⟨q, ⟨hqW, hqV⟩⟩ ↦ hb ⟨_, hqW⟩,
    fun ⟨q, ⟨hqW, hqV⟩⟩ ↦ ?_⟩
  ext
  specialize h_frac ⟨_, hqW⟩
  simp_all [comapStructureSheafFun]

Goal state after:
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:
by
  obtain ⟨ι, U, pres, hU, hU'⟩ := M.exists_isOpenCover_presentation
  refine ⟨Scheme.AffineOpenCover.ofIsOpenCover _ hU hU', fun i ↦ ⟨?_⟩⟩
  exact SheafOfModules.Presentation.ofIsIso.{u, u, u} ((restrictFunctorComp _ _).app M).inv <|
    (presentationRestrict (hU' i).isoSpec.inv (pres i))

Goal state after:
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
this✝ : IsUnit ((Subring.inclusion ⋯) ⟨x⁻¹, h⟩)
x' : ↥R.toLocalSubring.toSubring
hx' : ⟨x⁻¹, h⟩ * x' = 1
this : ↑x' = x
⊢ False

Tactic:
exact h' (this ▸ x'.2)

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 : ↑(CommRingCat.of (A⁰_ f))
p : ↥(unop (op (pbo f)))
⊢ HomogeneousLocalization.val (↑((awayToSection 𝒜 f).hom' x) p) =
    (IsLocalization.map (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) (RingHom.id A) ⋯)
      (HomogeneousLocalization.val x)

Tactic:
by
  obtain ⟨x, rfl⟩ := HomogeneousLocalization.mk_surjective x
  change (HomogeneousLocalization.mapId 𝒜 _ _).val = _
  dsimp [HomogeneousLocalization.mapId, HomogeneousLocalization.map]
  rw [Localization.mk_eq_mk', Localization.mk_eq_mk', IsLocalization.map_mk']
  rfl

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

Goal state before:
pp: case h₀
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
e₁ : pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
  Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd)) :=
  congrHom ⋯ ⋯ ≪≫ pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)
e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅ Spec (CommRingCat.of (Away 𝒜 (↑i.snd * ↑j.snd))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd →+* Away 𝒜 (↑i.snd * ↑j.snd) :=
  (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯).toRingHom
this : Function.Surjective ⇑F
x : ↑(CommRingCat.of (Away 𝒜 ↑i.snd))
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 ⋯ ⋯))) x =
    (CommRingCat.Hom.hom (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ CommRingCat.ofHom F)) x

Tactic:
exact DFunLike.congr_fun (Algebra.TensorProduct.lift_comp_includeLeft
      (awayMapₐ 𝒜 j.2.2 rfl) (awayMapₐ 𝒜 i.2.2 (mul_comm _ _)) (fun _ _ ↦ .all _ _)).symm x

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

Goal state before:
pp: case refine_4
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
⊢ ∀ (x : ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤))),
    (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) x = 0 → ∃ n, f ^ n • x = 0

Tactic:
· intro x hx
    obtain ⟨n, hn⟩ := h.uniqueness _ _ _ hx
    use n, hn

Goal state after:
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
Y : C
g : Y ⟶ B
⊢ (generateFamily X π).arrows g → (generate (Presieve.ofArrows X π)).arrows g

Tactic:
rintro ⟨a, g, rfl⟩

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
Y : C
a : α
g : Y ⟶ X a
⊢ (generate (Presieve.ofArrows X π)).arrows (g ≫ π a)
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
P Q : Sheaf J (Type v)
f g : P ⟶ Q
h : ∀ (X : C) (p : J.yoneda.obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g

Tactic:
by
  ext X x
  simpa only [yonedaEquiv_comp, Equiv.apply_symm_apply]
    using! congr_arg (J.yonedaEquiv) (h _ (J.yonedaEquiv.symm x))

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

Goal state before:
pp: case refine_1
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
z : X ⟶ c.pt
inst✝ : IsFiltered J
j : J
⊢ colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫ 𝟙 (colimit (pullback c.ι ((Functor.const J).map z))) ≫ f z =
    colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫
      colimMap (pullback.snd c.ι ((Functor.const J).map z)) ≫
        ((colimit.isColimit ((Functor.const J).obj X)).coconePointUniqueUpToIso (isColimitConstCocone J X)).hom

Tactic:
Category.id_comp,

Goal state after:
case refine_1
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
z : X ⟶ c.pt
inst✝ : IsFiltered J
j : J
⊢ colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫ f z =
    colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫
      colimMap (pullback.snd c.ι ((Functor.const J).map z)) ≫
        ((colimit.isColimit ((Functor.const J).obj X)).coconePointUniqueUpToIso (isColimitConstCocone J X)).hom
Module: Mathlib.Order.Interval.Set.Limit

Goal state before:
pp: case neg
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : ¬j ≤ b
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Tactic:
· simp only [not_le] at hb'
      refine ⟨j, hb', ?_⟩
      by_contra!
      apply hm.1
      rintro ⟨k, hk⟩ _
      exact this.trans (by simpa using hk)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous

Goal state before:
pp: case pos
C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type w
inst✝² : PartialOrder J✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : ↑(Set.Iio m) → ↑(Set.Iio ↑m) :=
  fun x ↦
    match x with
    | ⟨⟨a, ha⟩, ha'⟩ => ⟨a, ha'⟩
hf : Monotone f
j' : J
hj'✝ : j' ∈ Set.Iio ↑m
hj' : j' < ↑m
h : j' ≤ j
⊢ ∃ j₁, ⟨j', hj'✝⟩ ≤ ⟨↑j₁.1, ⋯⟩

pp: case neg
C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type w
inst✝² : PartialOrder J✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : ↑(Set.Iio m) → ↑(Set.Iio ↑m) :=
  fun x ↦
    match x with
    | ⟨⟨a, ha⟩, ha'⟩ => ⟨a, ha'⟩
hf : Monotone f
j' : J
hj'✝ : j' ∈ Set.Iio ↑m
hj' : j' < ↑m
h : j < j'
⊢ ∃ j₁, ⟨j', hj'✝⟩ ≤ ⟨↑j₁.1, ⋯⟩

Tactic:
· refine ⟨⟨⟨j, le_refl j⟩, ?_⟩, h⟩
        by_contra h'
        simp only [Set.mem_Iio, not_lt] at h'
        apply hm.1
        rintro ⟨k, hk⟩ hkm
        exact h'.trans hk

Goal state after:
case neg
C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type w
inst✝² : PartialOrder J✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : ↑(Set.Iio m) → ↑(Set.Iio ↑m) :=
  fun x ↦
    match x with
    | ⟨⟨a, ha⟩, ha'⟩ => ⟨a, ha'⟩
hf : Monotone f
j' : J
hj'✝ : j' ∈ Set.Iio ↑m
hj' : j' < ↑m
h : j < j'
⊢ ∃ j₁, ⟨j', hj'✝⟩ ≤ ⟨↑j₁.1, ⋯⟩
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
x✝ : Discrete c.ι
i : c.ι
⊢ c.cofan₁.ι.app { as := i } ≫ c.m =
    c.cofan₁.ι.app { as := i } ≫
      c.isColimit₁.desc
        { pt := c.cofan₂.pt,
          ι :=
            (Discrete.natTrans fun x ↦
                match x with
                | { as := i } => g (c.π i)) ≫
              c.cofan₂.ι }

Tactic:
rw [IsColimit.fac]; exact c.hm i

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case succ.inr.inl
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂✝ : k₂ ≤ Order.succ j
h₀ : j ≤ Order.succ j
hj₂ : restrictionLE iter₁.F h₀ = restrictionLE iter₂.F h₀
hsucc : iter₁.F.obj ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), k₂ ≤ j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
h : ¬k₂ ≤ j
h₂ : k₂ < Order.succ j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂✝

Tactic:
exact this _ _ _ _ ((Order.lt_succ_iff_of_not_isMax hj₁).1 h₂)

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
inst✝¹ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝ : HasPushout (functorObjTop f πY) (functorObjLeft f πY)
⊢ ιFunctorObj f πX ≫ functorMap f τ = Arrow.Hom.left τ ≫ ιFunctorObj f πY

Tactic:
by
  simp [ιFunctorObj, functorMap]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
⊢ (extendToSucc hj F τ).map (homOfLE hi) ≫ (extendToSuccObjIso hj F τ i₂ hi₂).hom =
    (extendToSuccObjIso hj F τ i₁ ⋯).hom ≫ F.map (homOfLE hi)

Tactic:
dsimp [extendToSucc, extendToSuccObjIso]
  rw [extendToSucc.map_eq _ _ _ _ _ _ hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
e : d.Extension val₀ j
i : J
e' : d.Extension val₀ i
h : i ≤ j
⊢ (ConcreteCategory.hom (F.map (homOfLE h).op)) e.val = e'.val

Tactic:
by
  obtain rfl : e' = e.ofLE h := Subsingleton.elim _ _
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case e'_2
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩) =
    (ConcreteCategory.hom (𝟙 (F.obj (op (Order.succ i))))) (e (Order.succ i) ⋯).val

Tactic:
id_apply,

Goal state after:
case e'_2
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩) = (e (Order.succ i) ⋯).val
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
val₀ : F.obj (op ⊥)
j✝ j'✝ : Jᵒᵖ
f : j✝ ⟶ j'✝
⊢ (ConcreteCategory.hom (F.map f)) ((fun j ↦ default.val) j✝) = (fun j ↦ default.val) j'✝

Tactic:
by apply Extension.compatibility

Goal state after: