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

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral).RespectsIso
⊢ IsIntegralHom (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).IsIntegral

Tactic:
HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom),

Goal state after:
R S : CommRingCat
φ : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral).RespectsIso
⊢ IsAffine (Spec S) ∧ (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map φ) ⊤)).IsIntegral ↔
    (CommRingCat.Hom.hom φ).IsIntegral
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

Tactic:
HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom),

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite ↔
    (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤)).IsIntegral) ∧ LocallyOfFiniteType f
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x✝ y✝ x y : (j : J) × F.obj j
f : x.fst ⟶ y.fst
h : y.snd = (ConcreteCategory.hom (F.map f)) x.snd
⊢ (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map (𝟙 y.fst))) y.snd

Tactic:
by simpa using h.symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), (𝒰.X i).IsGermInjective
x : ↥X
⊢ X.IsGermInjectiveAt x

Tactic:
← (𝒰.covers x).choose_spec

Goal state after:
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), (𝒰.X i).IsGermInjective
x : ↥X
⊢ X.IsGermInjectiveAt ((𝒰.f (Cover.idx 𝒰 x)) (Exists.choose ⋯))
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
s : Finset ↑R
hs : Ideal.span ↑s = J
hs' : ↑s ⊆ ↑J
x y : ↑R
e : y * x = 0
hy : y ∉ I
i : ↑R
hi : i ∈ ↑s
⊢ ↑(∏ x ∈ s.attach, f ↑x ⋯) ∈ (↑R ∙ i).annihilator

Tactic:
Submonoid.coe_finsetProd

Goal state after:
X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
s : Finset ↑R
hs : Ideal.span ↑s = J
hs' : ↑s ⊆ ↑J
x y : ↑R
e : y * x = 0
hy : y ∉ I
i : ↑R
hi : i ∈ ↑s
⊢ ∏ i ∈ s.attach, ↑(f ↑i ⋯) ∈ (↑R ∙ i).annihilator
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case e_a
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
⊢ Scheme.Hom.resLE f V U ⋯ = Scheme.Hom.resLE g V U ⋯

Tactic:
have : IsAffine V := hV

Goal state after:
case e_a
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
this : IsAffine ↑V
⊢ Scheme.Hom.resLE f V U ⋯ = Scheme.Hom.resLE g V U ⋯
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
hX : IrreducibleSpace ↥X
inst✝ : IrreducibleSpace ↥Y
⊢ f (genericPoint ↥X) = genericPoint ↥Y

Tactic:
apply ((genericPoint_spec Y).eq _).symm

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
hX : IrreducibleSpace ↥X
inst✝ : IrreducibleSpace ↥Y
⊢ IsGenericPoint (f (genericPoint ↥X)) Set.univ
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact ↑UX
I : Set ↑X.affineOpens
hI : I.Finite
e : UX = ⨆ i ∈ I, ↑i
⊢ Mono (pushoutSection H hUST hUSX hUY)

Tactic:
have := hI.to_subtype

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact ↑UX
I : Set ↑X.affineOpens
hI : I.Finite
e : UX = ⨆ i ∈ I, ↑i
this : Finite ↑I
⊢ Mono (pushoutSection H hUST hUSX hUY)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
I : Set ↑X.affineOpens
hI : I.Finite
e : UX = ⨆ i ∈ I, ↑i
hIUX : ∀ (i : ↑I), ↑↑i ≤ UX
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
have := hI.to_subtype

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
I : Set ↑X.affineOpens
hI : I.Finite
e : UX = ⨆ i ∈ I, ↑i
hIUX : ∀ (i : ↑I), ↑↑i ≤ UX
this : Finite ↑I
⊢ IsIso (pushoutSection H hUST hUSX hUY)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat iX
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUX : IsCompact ↑UX
hf : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
I : Set ↑X.affineOpens
hI : I.Finite
e : UX = ⨆ i ∈ I, ↑i
⊢ Mono (pushoutSection H hUST hUSX hUY)

Tactic:
have := hI.to_subtype

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat iX
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUX : IsCompact ↑UX
hf : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
I : Set ↑X.affineOpens
hI : I.Finite
e : UX = ⨆ i ∈ I, ↑i
this : Finite ↑I
⊢ Mono (pushoutSection H hUST hUSX hUY)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUX : IsCompact ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
⊢ Mono (pushoutSection ⋯ hUSX hUST ⋯)

Tactic:
exact mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat _ _ _ _ hUS hUX hUT hiX

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

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
I : Set ↑T.affineOpens
hI : I.Finite
e : UT = ⨆ i ∈ I, ↑i
hIUT : ∀ (i : ↑I), ↑↑i ≤ UT
⊢ IsIso (pushoutSection ⋯ hUSX hUST ⋯)

Tactic:
have := hI.to_subtype

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
I : Set ↑T.affineOpens
hI : I.Finite
e : UT = ⨆ i ∈ I, ↑i
hIUT : ∀ (i : ↑I), ↑↑i ≤ UT
this : Finite ↑I
⊢ IsIso (pushoutSection ⋯ hUSX hUST ⋯)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_2
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact ↑U
hV : IsCompact ↑V
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
j₂ : I
fj₂i : j₂ ⟶ i
e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U
k : I
fkj₁ : k ⟶ j₁
fkj₂ : k ⟶ j₂
e : fkj₁ ≫ fj₁i = fkj₂ ≫ fj₂i
⊢ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ V ≤ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ U

Tactic:
· rw [e]
    simpa only [Scheme.Hom.comp_preimage, Functor.map_comp] using Scheme.Hom.preimage_mono _ e₂

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅ pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) :=
  pullbackRightPullbackFstIso f (𝒰.f j) (pullback.fst f (𝒰.f i)) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫ pullbackAssoc f (𝒰.f i) (𝒰.f i) (𝒰.f j)
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
      (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ =
    pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y) (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯)
        (𝟙 X) ⋯ ⋯ ≫
      iso.inv

Tactic:
apply pullback.hom_ext

Goal state after:
case h₀
P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅
  pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) := ⋯
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
        (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ ≫
      pullback.fst (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) =
    (pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y) (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯)
          (𝟙 X) ⋯ ⋯ ≫
        iso.inv) ≫
      pullback.fst (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))

case h₁
P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅
  pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) := ⋯
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
        (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ ≫
      pullback.snd (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) =
    (pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y) (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯)
          (𝟙 X) ⋯ ⋯ ≫
        iso.inv) ≫
      pullback.snd (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.310} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
hij : i ⟶ j
iso : pullback f (𝒰.f i) ≅ pullback (pullback.snd f (𝒰.f j)) (𝒰.trans hij) :=
  pullback.congrHom ⋯ ⋯ ≪≫ (pullbackLeftPullbackSndIso f (𝒰.f j) (𝒰.trans hij)).symm
⊢ (pullbackLeftPullbackSndIso f (𝒰.f j) (𝒰.trans hij)).hom ≫
      pullback.map f (𝒰.trans hij ≫ 𝒰.f j) f (𝒰.f i) (𝟙 Y) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯ ≫
        pullback.map f (𝒰.f i) f (𝒰.f j) (𝟙 Y) (𝒰.trans hij) (𝟙 X) ⋯ ⋯ =
    pullback.fst (pullback.snd f (𝒰.f j)) (𝒰.trans hij)

Tactic:
apply pullback.hom_ext

Goal state after:
case h₀
P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.310} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
hij : i ⟶ j
iso : pullback f (𝒰.f i) ≅ pullback (pullback.snd f (𝒰.f j)) (𝒰.trans hij) := ⋯
⊢ ((pullbackLeftPullbackSndIso f (𝒰.f j) (𝒰.trans hij)).hom ≫
        pullback.map f (𝒰.trans hij ≫ 𝒰.f j) f (𝒰.f i) (𝟙 Y) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯ ≫
          pullback.map f (𝒰.f i) f (𝒰.f j) (𝟙 Y) (𝒰.trans hij) (𝟙 X) ⋯ ⋯) ≫
      pullback.fst f (𝒰.f j) =
    pullback.fst (pullback.snd f (𝒰.f j)) (𝒰.trans hij) ≫ pullback.fst f (𝒰.f j)

case h₁
P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.310} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
hij : i ⟶ j
iso : pullback f (𝒰.f i) ≅ pullback (pullback.snd f (𝒰.f j)) (𝒰.trans hij) := ⋯
⊢ ((pullbackLeftPullbackSndIso f (𝒰.f j) (𝒰.trans hij)).hom ≫
        pullback.map f (𝒰.trans hij ≫ 𝒰.f j) f (𝒰.f i) (𝟙 Y) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯ ≫
          pullback.map f (𝒰.f i) f (𝒰.f j) (𝟙 Y) (𝒰.trans hij) (𝟙 X) ⋯ ⋯) ≫
      pullback.snd f (𝒰.f j) =
    pullback.fst (pullback.snd f (𝒰.f j)) (𝒰.trans hij) ≫ pullback.snd f (𝒰.f j)
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: J : Type u_1
inst✝² : Category.{u_2, u_1} J
F G : J ⥤ Scheme
s : F ⟶ G
inst✝¹ : Quiver.IsThin J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective ⇑(F.map hij)
inst✝ : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq : (F.map fi) xi = (F.map fj) xj
⊢ (s.app i ≫ G.map fi) xi = (G.map fj) ((s.app j) xj)

Tactic:
← s.naturality,

Goal state after:
J : Type u_1
inst✝² : Category.{u_2, u_1} J
F G : J ⥤ Scheme
s : F ⟶ G
inst✝¹ : Quiver.IsThin J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective ⇑(F.map hij)
inst✝ : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq : (F.map fi) xi = (F.map fj) xj
⊢ (F.map fi ≫ s.app k) xi = (G.map fj) ((s.app j) xj)
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: J : Type u_1
inst✝² : Category.{u_2, u_1} J
F G : J ⥤ Scheme
s : F ⟶ G
inst✝¹ : Quiver.IsThin J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective ⇑(F.map hij)
inst✝ : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq : (F.map fi) xi = (F.map fj) xj
⊢ (F.map fj ≫ s.app k) xj = (G.map fj) ((s.app j) xj)

Tactic:
s.naturality

Goal state after:
J : Type u_1
inst✝² : Category.{u_2, u_1} J
F G : J ⥤ Scheme
s : F ⟶ G
inst✝¹ : Quiver.IsThin J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective ⇑(F.map hij)
inst✝ : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq : (F.map fi) xi = (F.map fj) xj
⊢ (s.app j ≫ G.map fj) xj = (G.map fj) ((s.app j) xj)
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : 𝒰.I₀
xj : ↥(d.functor.obj j)
x✝ : (colimit.ι d.functor j) xj ∈ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i)
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h✝ : (trans 𝒰 fj) uk = (d.natTrans.app j) xj
h : (𝒰.f i) ((trans 𝒰 fi) uk) = d.toBase ((colimit.ι d.functor j) xj)
⊢ (𝒰.f j) ((d.natTrans.app j) xj) = (𝒰.f j) (((functorOfLocallyDirected 𝒰).map fj) uk)

Tactic:
simp only [functorOfLocallyDirected_obj, functorOfLocallyDirected_map]

Goal state after:
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : 𝒰.I₀
xj : ↥(d.functor.obj j)
x✝ : (colimit.ι d.functor j) xj ∈ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i)
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h✝ : (trans 𝒰 fj) uk = (d.natTrans.app j) xj
h : (𝒰.f i) ((trans 𝒰 fi) uk) = d.toBase ((colimit.ι d.functor j) xj)
⊢ (𝒰.f j) ((d.natTrans.app j) xj) = (𝒰.f j) ((trans 𝒰 fj) uk)
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : 𝒰.I₀
xj : ↥(d.functor.obj j)
x✝ : (colimit.ι d.functor j) xj ∈ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i)
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h✝ : (trans 𝒰 fj) uk = (d.natTrans.app j) xj
h : (𝒰.f i) ((trans 𝒰 fi) uk) = d.toBase ((colimit.ι d.functor j) xj)
⊢ (d.natTrans.app j) xj = ((functorOfLocallyDirected 𝒰).map fj) uk

Tactic:
by
      apply (𝒰.f j).injective
      simp only [functorOfLocallyDirected_obj, functorOfLocallyDirected_map]
      rw [← Scheme.Hom.comp_apply, ← ι_toBase, Scheme.Hom.comp_apply, ← h]
      simp [← Scheme.Hom.comp_apply]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case ht
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : c.val i = 1
⊢ 0 < c.degBound

Tactic:
InductionObj.degBound

Goal state after:
case ht
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : c.val i = 1
⊢ 0 < ∑ i, (c.val i).degree.succ