mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
i : ι
hi : (ConcreteCategory.hom (F.map g)) x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
this✝ : HasPullback g (f i)
this : F.map (p₁ i) = F.map ⋯.isoPullback.hom ≫ pullbackComparison F g (f i) ≫ pullback.fst (F.map g) (F.map (f i))
⊢ x ∈
    ⇑(ConcreteCategory.hom (pullback.fst (F.map g) (F.map (f i)))) ''
      Set.range
        (⇑(ConcreteCategory.hom (pullbackComparison F g (f i))) ∘ ⇑(ConcreteCategory.hom (F.map ⋯.isoPullback.hom)))

Tactic:
Function.Surjective.range_eq <| (H _ _).comp (surjective_of_epi _),

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
i : ι
hi : (ConcreteCategory.hom (F.map g)) x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
this✝ : HasPullback g (f i)
this : F.map (p₁ i) = F.map ⋯.isoPullback.hom ≫ pullbackComparison F g (f i) ≫ pullback.fst (F.map g) (F.map (f i))
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.fst (F.map g) (F.map (f i)))) '' Set.univ
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
T : C
g✝ : T ⟶ S
W : ι → C
p₁ : (i : ι) → W i ⟶ T
p₂ : (i : ι) → W i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g✝ (f i)
Z : C
g : Z ⟶ T
hg : Presieve.ofArrows W p₁ g
⊢ P g

Tactic:
obtain ⟨i⟩ := hg

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
T : C
g : T ⟶ S
W : ι → C
p₁ : (i : ι) → W i ⟶ T
p₂ : (i : ι) → W i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
Y : C
i : ι
⊢ P (p₁ i)
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: case mpr
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y ∧
      (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y →
    (ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) = y

Tactic:
rintro ⟨e₁, e₂⟩

Goal state after:
case mpr
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
e₁ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) = y
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
⊢ Opens.IsBasis (Set.range X.basicOpen)

Tactic:
by
  convert!
    PrimeSpectrum.isBasis_basic_opens.of_isInducing
      (TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)).isInducing using 1
  ext V
  simp only [Set.mem_range, exists_exists_eq_and, Set.mem_ofPred,
    ← Opens.coe_inj (V := V), ← Scheme.toSpecΓ_preimage_basicOpen]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: case init.init
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
⊢ ∀ (xi xj : F.obj none),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

Tactic:
simp only [((CategoryTheory.mono_iff_injective (F.map (.init i))).mp inferInstance).eq_iff,
      forall_eq']

Goal state after:
case init.init
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
⊢ ∀ (xi : F.obj none),
    ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xi
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝² : K.HasPullbacks
inst✝¹ : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
inst✝ : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
⊢ P f

Tactic:
rw [IsLocalAtTarget.iff_of_zeroHypercover (P := P) 𝒰.restrictIndexOfSmall]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝² : K.HasPullbacks
inst✝¹ : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
inst✝ : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
⊢ ∀ (i : 𝒰.restrictIndexOfSmall.I₀), P (pullback.snd f (𝒰.restrictIndexOfSmall.f i))
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom

Tactic:
have eq₁ := D.t_fac i i j

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = pullback.fst (D.f i i) (D.f i j) ≫ D.t i i
⊢ D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X A B Y : C
f : X ⟶ Y
gA : A ⟶ Y
gB : B ⟶ Y
⊢ Hom.left (prodComparisonIso (pullback f) (mk gA) (mk gB)).inv ≫
      pullback.fst (pullback.fst gA gB ≫ gA) f ≫ pullback.snd gA gB =
    pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom ≫ pullback.fst (mk gB).hom f

Tactic:
by
  rw [← cancel_epi (prodComparisonIso (Over.pullback f) _ _).hom.left,
    Over.hom_left_inv_left_assoc]
  simp [CartesianMonoidalCategory.prodComparison, snd]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasPullbacks C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst✝ : MonObj (mk f)
⊢ MonObj.mul ≫ homMk (pullback.fst f (𝟙 X)) ⋯ =
    (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯) ≫ MonObj.mul

Tactic:
by
    ext
    dsimp [monObjMkPullbackSnd_mul]
    simp only [Category.assoc, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
    simp only [← Category.assoc]
    congr 1
    ext <;> simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
i : ι
x : ↥(f i)
⊢ colimit.ι (Discrete.functor fun x ↦ (f x).toTopCat) { as := i } ≫
      (PreservesCoproduct.iso Scheme.forgetToTop f).symm.hom =
    Scheme.forgetToTop.map (Sigma.ι f i)

Tactic:
exact ι_comp_sigmaComparison Scheme.forgetToTop _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
⊢ { I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
        f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings (pullback f g)

Tactic:
rw [ofArrows_mem_precoverage_iff]

Goal state after:
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
⊢ (∀ (x : ↥(pullback f g)),
      ∃ i,
        x ∈
          Set.range
            ⇑({ I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
                    f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.f
                i)) ∧
    ∀
      (i :
        { I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
            f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.I₀),
      IsOpenImmersion
        ({ I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
              f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.f
          i)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (D.f i i).base)

Tactic:
rw [← TopCat.epi_iff_surjective]
      infer_instance

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

Goal state before:
pp: P : AffineTargetMorphismProperty
h₁ : ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], P f → P (e.hom ≫ f)
h₂ : ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], P f → P (f ≫ e.hom)
⊢ P.toProperty.RespectsIso

Tactic:
by
  apply MorphismProperty.RespectsIso.mk
  · rintro X Y Z e f ⟨a, h⟩; exact ⟨a, h₁ e f h⟩
  · rintro X Y Z e f ⟨a, h⟩; exact ⟨.of_isIso e.inv, h₂ e f h⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
⊢ IsIso (pullback.lift fWX fWY h)

Tactic:
have H₁ (i : _) : IsIso ((openCoverOfLeft 𝒰 fXZ fYZ).pullbackHom (lift fWX fWY h) i) := by
    let f := map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) (by simp) (by simp)
    have : IsPullback (fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (fst _ _) := by
      simpa [← IsPullback.paste_vert_iff (.of_hasPullback _ _), f] using .of_hasPullback _ _
    have H' : IsPullback (fst fWX (𝒰.f i)) (lift (snd _ _) (fst _ _ ≫ fWY) (by simp [← h]))
        (lift fWX fWY h) f := by
      rw [← IsPullback.paste_vert_iff this.flip (by ext <;> simp [f])]
      simpa using .of_hasPullback _ _
    convert! (inferInstance : IsIso (H'.isoPullback.inv ≫ (H i).isoPullback.hom))
    aesop (add simp [Iso.eq_inv_comp, Scheme.Cover.pullbackHom])

Goal state after:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
H₁ :
  ∀ (i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1),
    IsIso (Cover.pullbackHom (openCoverOfLeft 𝒰 fXZ fYZ) (pullback.lift fWX fWY h) i)
⊢ IsIso (pullback.lift fWX fWY h)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
s : Cocone F
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
refine (Category.assoc _ _ _).trans ?_

Goal state after:
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
s : Cocone F
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
⊢ s.fst.base ≫ (forget C).map (D.ι i) ≫ (D.gluedIso (forget C)).hom = s.snd.base ≫ D.toTopGlueData.ι j

Tactic:
←
          𝖣.ι_gluedIso_hom (PresheafedSpace.forget _) _

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
⊢ s.fst.base ≫ (forget C).map (D.ι i) ≫ (D.gluedIso (forget C)).hom =
    s.snd.base ≫ (forget C).map (D.ι j) ≫ (D.gluedIso (forget C)).hom
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
⊢ s.fst.base ≫ (forget C).map (D.ι i) ≫ (D.gluedIso (forget C)).hom =
    s.snd.base ≫ (forget C).map (D.ι j) ≫ (D.gluedIso (forget C)).hom

Tactic:
have := congr_arg PresheafedSpace.Hom.base s.condition

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
this : (s.fst ≫ D.ι i).base = (s.snd ≫ D.ι j).base
⊢ s.fst.base ≫ (forget C).map (D.ι i) ≫ (D.gluedIso (forget C)).hom =
    s.snd.base ≫ (forget C).map (D.ι j) ≫ (D.gluedIso (forget C)).hom
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsDominant x✝ ↔ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ DenseRange) x✝

Tactic:
exact isDominant_iff _

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

Goal state before:
pp: case of_sSup_eq_top
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (f ∣_ U i)
X' Y' : Scheme
⊢ ∀ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → P f'

Tactic:
i₁

Goal state after:
case of_sSup_eq_top
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
⊢ ∀ (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → P f'
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
rₐ : (a : ↑s) → Localization.Away ↑a := fun a ↦ (algebraMap S (Localization.Away ↑a)) (f r)
Sₐ : ↑s → Type u := fun a ↦ Localization.Away (rₐ a)
⊢ ∃ ι s,
    ∃ (_ : Ideal.span (Set.range s) = ⊤),
      ∃ Sₜ x x_1,
        ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
          ∀ (i : ι), P ((algebraMap S' (Sₜ i)).comp (IsLocalization.Away.map R' S' f r))

Tactic:
have (a : s) :
      IsLocalization.Away (((algebraMap S (Localization.Away a.val)).comp f) r) (Sₐ a) :=
    inferInstanceAs (IsLocalization.Away (rₐ a) (Sₐ a))

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
rₐ : (a : ↑s) → Localization.Away ↑a := fun a ↦ (algebraMap S (Localization.Away ↑a)) (f r)
Sₐ : ↑s → Type u := fun a ↦ Localization.Away (rₐ a)
this : ∀ (a : ↑s), IsLocalization.Away (((algebraMap S (Localization.Away ↑a)).comp f) r) (Sₐ a)
⊢ ∃ ι s,
    ∃ (_ : Ideal.span (Set.range s) = ⊤),
      ∃ Sₜ x x_1,
        ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
          ∀ (i : ι), P ((algebraMap S' (Sₜ i)).comp (IsLocalization.Away.map R' S' f r))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ P
    (CommRingCat.Hom.hom
      (Scheme.Hom.appTop
        ((PreservesPullback.iso AffineScheme.forgetToScheme (AffineScheme.ofHom f) (AffineScheme.ofHom g)).inv ≫
          AffineScheme.forgetToScheme.map (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)))))

Tactic:
rw [Scheme.Hom.comp_appTop, CommRingCat.hom_comp, hP'.cancel_right_isIso,
    AffineScheme.forgetToScheme_map]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)).hom))
Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
x✝¹ : HasPullback f g
x✝ : IsPreimmersion g
⊢ IsPreimmersion (pullback.fst f g)

Tactic:
have := pullback_fst (P := @SurjectiveOnStalks) f g inferInstance

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
x✝¹ : HasPullback f g
x✝ : IsPreimmersion g
this : SurjectiveOnStalks (pullback.fst f g)
⊢ IsPreimmersion (pullback.fst f g)
Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
x✝¹ : HasPullback f g
x✝ : IsPreimmersion g
this✝ : SurjectiveOnStalks (pullback.fst f g)
L : ↥(pullback f g) → ↑{x | f x.1 = g x.2} := fun x ↦ ⟨((pullback.fst f g) x, (pullback.snd f g) x), ⋯⟩
this : IsEmbedding L
⊢ IsEmbedding ⇑(pullback.fst f g)

Tactic:
exact IsEmbedding.subtypeVal.comp ((TopCat.pullbackHomeoPreimage _ f.continuous _
    g.isEmbedding).isEmbedding.comp this)

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

Goal state before:
pp: X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))
this✝ : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
this : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsAffine ((X.openCoverOfIsOpenCover U hU).X i)
i j : (X.openCoverOfIsOpenCover U hU).I₀
⊢ IsCompact Set.univ

Tactic:
(pullback.fst ((X.openCoverOfIsOpenCover U hU).f i)
    ((X.openCoverOfIsOpenCover U hU).f j) ≫
    (X.openCoverOfIsOpenCover U hU).f i).isOpenEmbedding.isCompact_iff,

Goal state after:
X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))
this✝ : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
this : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsAffine ((X.openCoverOfIsOpenCover U hU).X i)
i j : (X.openCoverOfIsOpenCover U hU).I₀
⊢ IsCompact
    (⇑(pullback.fst ((X.openCoverOfIsOpenCover U hU).f i) ((X.openCoverOfIsOpenCover U hU).f j) ≫
          (X.openCoverOfIsOpenCover U hU).f i) ''
      Set.univ)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
x : ↑Γ(X, X.basicOpen f)
⊢ ∃ n y, (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x

Tactic:
have := (hU.isLocalization_basicOpen f).1.2
  obtain ⟨⟨y, _, n, rfl⟩, d⟩ := this x
  use n, y
  simpa [mul_comm x] using! d.symm

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R x ↦ IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
x : R
hx : IsNilpotent x
J : Ideal R
hJ : J.IsMaximal
⊢ (algebraMap R (Localization.AtPrime J)) x = 0

Tactic:
specialize h J hJ

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
hx : IsNilpotent x
J : Ideal R
hJ : J.IsMaximal
h : IsReduced (Localization.AtPrime J)
⊢ (algebraMap R (Localization.AtPrime J)) x = 0
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this : p.IsPrime
h : ¬p.height = ⊤
⊢ ↑(r + 1) ≤ p.height

Tactic:
have : p.FiniteHeight := ⟨Or.inr h⟩

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this✝ : p.IsPrime
h : ¬p.height = ⊤
this : p.FiniteHeight
⊢ ↑(r + 1) ≤ p.height