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

Goal state before:
pp: X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
⊢ IsAffineOpen (Scheme.Hom.opensRange (pullback.fst f₁ f₂ ≫ f₁))

Tactic:
convert! H _ _ (isAffineOpen_opensRange f₁) (isAffineOpen_opensRange f₂)

Goal state after:
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
⊢ Scheme.Hom.opensRange (pullback.fst f₁ f₂ ≫ f₁) = Scheme.Hom.opensRange f₁ ⊓ Scheme.Hom.opensRange f₂
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: ⊢ StableUnderComposition @Finite

Tactic:
introv R hf hg

Goal state after:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.Finite
hg : g.Finite
⊢ (g.comp f).Finite
Module: Mathlib.RingTheory.RingHom.FiniteType

Goal state before:
pp: ⊢ StableUnderComposition @FiniteType

Tactic:
introv R hf hg

Goal state after:
R S T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FiniteType
hg : g.FiniteType
⊢ (g.comp f).FiniteType
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔ IsPreimmersion f ∧ IsClosed (Set.range ⇑f)

Tactic:
by
  rw [isClosedImmersion_iff, isPreimmersion_iff, and_assoc, isClosedEmbedding_iff]

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst✝¹ : IsClosedImmersion iX
inst✝ : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
⊢ Hom.ker iX = Hom.ker (pullback.fst f iY)

Tactic:
ker_fst_of_isClosedImmersion,

Goal state after:
ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst✝¹ : IsClosedImmersion iX
inst✝ : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
⊢ Hom.ker iX = (Hom.ker iY).comap f
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: ⊢ StableUnderComposition @FinitePresentation

Tactic:
introv R hf hg

Goal state after:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FinitePresentation
hg : g.FinitePresentation
⊢ (g.comp f).FinitePresentation
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒱 i).I₀), IsAffine ((𝒱 i).X j)
U : (i : 𝒰.I₀) × (𝒱 i).I₀ → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i ↦ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)
i : (i : 𝒰.I₀) × (𝒱 i).I₀
⊢ Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩) ≤ diagonalCoverDiagonalRange f 𝒰 𝒱

Tactic:
exact le_iSup (fun i : Σ i, (𝒱 i).I₀ ↦ ((diagonalCover f 𝒰 𝒱).f ⟨i.1, i.2, i.2⟩).opensRange) i

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

Goal state before:
pp: W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
⊢ f = g

Tactic:
let g' : X' ⟶ Y' := Over.homMk g

Goal state after:
W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
⊢ f = g
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y Z : Scheme
⊢ HasAffineProperty @IsClosedImmersion fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Tactic:
convert! HasAffineProperty.of_isZariskiLocalAtTarget @IsClosedImmersion

Goal state after:
case e'_2
X Y Z : Scheme
x✝³ x✝² : Scheme
x✝¹ : x✝³ ⟶ x✝²
x✝ : IsAffine x✝²
⊢ IsAffine x✝³ ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop x✝¹)) ↔
    AffineTargetMorphismProperty.of (@IsClosedImmersion) x✝¹
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : PrimeSpectrum R
⊢ comap C (comap (evalRingHom 0) x) = x

Tactic:
rw [← comap_comp_apply, (show (evalRingHom 0).comp C = .id R by ext; simp),
    comap_id]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsDominant f
inst✝ : IsReduced Y
⊢ Set.range ⇑f ⊆ ↑(Scheme.Hom.ker f).support

Tactic:
exact f.range_subset_ker_support

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : IsLocallyNoetherian Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
this✝ : IsReduced (Y.affineCover.X i)
this : IsNoetherian (Y.affineCover.X i) :=
  { toIsLocallyNoetherian := instIsLocallyNoetherianXScheme i,
    toCompactSpace := Scheme.compactSpace_of_isAffine (Y.affineCover.X i) }
⊢ Finite ↑(irreducibleComponents ↥(Y.affineCover.X i))

Tactic:
exact TopologicalSpace.NoetherianSpace.finite_irreducibleComponents

Goal state after:
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: ⊢ StableUnderComposition fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral

Tactic:
introv R hf hg

Goal state after:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.IsIntegral
hg : g.IsIntegral
⊢ (g.comp f).IsIntegral
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this : ∀ {X Y : Scheme} {f : X ⟶ Y}, UniversallyClosed f → IsAffineHom f → (∃ R, Y = Spec R) → IsIntegralHom f
hY : ¬∃ R, Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
IsZariskiLocalAtTarget.iff_of_openCover (P := @UniversallyClosed) Y.affineCover

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
H₁ : ∀ (i : Y.affineCover.toPreZeroHypercover.1), UniversallyClosed (Scheme.Cover.pullbackHom Y.affineCover f i)
H₂ : IsAffineHom f
this : ∀ {X Y : Scheme} {f : X ⟶ Y}, UniversallyClosed f → IsAffineHom f → (∃ R, Y = Spec R) → IsIntegralHom f
hY : ¬∃ R, Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
R : CommRingCat
inst✝¹ : Subsingleton ↥(Spec R)
inst✝ : IsReduced (Spec R)
h✝ : Nonempty ↥(Spec R)
this✝ : IrreducibleSpace ↥(Spec R)
this : IsDomain ↑R
φ : S ⟶ R
⊢ (CommRingCat.Hom.hom φ).Finite ↔ (CommRingCat.Hom.hom φ).FiniteType

Tactic:
have := (PrimeSpectrum.t1Space_iff_isField (R := R)).mp (show T1Space (Spec R) by infer_instance)

Goal state after:
case inr
S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
R : CommRingCat
inst✝¹ : Subsingleton ↥(Spec R)
inst✝ : IsReduced (Spec R)
h✝ : Nonempty ↥(Spec R)
this✝¹ : IrreducibleSpace ↥(Spec R)
this✝ : IsDomain ↑R
φ : S ⟶ R
this : IsField ↑R
⊢ (CommRingCat.Hom.hom φ).Finite ↔ (CommRingCat.Hom.hom φ).FiniteType
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case refine_1
R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst✝² : Flat (Spec.map φ)
inst✝¹ : QuasiCompact (Spec.map φ)
inst✝ : Surjective (Spec.map φ)
hs : IsOpen (⇑(Spec.map φ) ⁻¹' s)
⊢ Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))

Tactic:
exact (surjective_iff (Spec.map φ)).mp inferInstance

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    apply (ΓSpec.adjunction.homEquiv _ _).symm.injective
    apply Quiver.Hom.unop_inj
    rw [Adjunction.homEquiv_symm_apply, Adjunction.homEquiv_symm_apply]
    dsimp
    simp only [Scheme.toSpecΓ_appTop, Scheme.ΓSpecIso_naturality, Iso.inv_hom_id_assoc]
    apply of_mvPolynomial_int_ext
    intro i
    rw [ConcreteCategory.hom_ofHom, coe_eval₂Hom, eval₂_X]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f✝ : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f✝.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j : I
f : I → (s.pt ⟶ cF.pt) := fun i ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
this : ∀ (i j : I), f i = f j
⊢ ⋯.lift (s.π.app (Classical.arbitrary I)) (hcG.lift ((Cone.postcompose α).obj s)) ⋯ ≫ cF.π.app j = s.π.app j

Tactic:
change f _ ≫ _ = _

Goal state after:
I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f✝ : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f✝.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j : I
f : I → (s.pt ⟶ cF.pt) := fun i ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
this : ∀ (i j : I), f i = f j
⊢ f (Classical.arbitrary I) ≫ cF.π.app j = s.π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j : I
⊢ ⋯.lift (s.π.app (Classical.arbitrary I)) (hcG.lift ((Cone.postcompose α).obj s)) ⋯ ≫ cF.π.app j = s.π.app j

Tactic:
let f (i : _) : s.pt ⟶ cF.pt :=
      (hf i).lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) (by simp)
    have (i j : _) : f i = f j := by
      refine constant_of_preserves_morphisms f (fun j₁ j₂ g ↦ ?_) i j
      refine (hf j₂).hom_ext ?_ (by simp [f])
      rw [IsPullback.lift_fst, ← cF.w g, IsPullback.lift_fst_assoc, Cone.w]
    change f _ ≫ _ = _
    rw [this _ j]
    simp [f]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
this : IsIso (terminal.from (Spec (CommRingCat.of (ULift.{?u.14, 0} ℤ))))
⊢ Surjective (terminal.from (Spec ℤ[n]))

Tactic:
← terminal.comp_from (Spec.map (CommRingCat.ofHom C)),

Goal state after:
n : Type u
S : Scheme
this : IsIso (terminal.from (Spec (CommRingCat.of (ULift.{?u.14, 0} ℤ))))
⊢ Surjective (Spec.map (CommRingCat.ofHom C) ≫ terminal.from (Spec (CommRingCat.of (ULift.{u, 0} ℤ))))
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
inst✝ : Finite n
this : IsIso (terminal.from (Spec (CommRingCat.of (ULift.{u, 0} ℤ))))
⊢ LocallyOfFinitePresentation (terminal.from (Spec ℤ[n]))

Tactic:
← terminal.comp_from (Spec.map (CommRingCat.ofHom C)),

Goal state after:
n : Type u
S : Scheme
inst✝ : Finite n
this : IsIso (terminal.from (Spec (CommRingCat.of (ULift.{u, 0} ℤ))))
⊢ LocallyOfFinitePresentation (Spec.map (CommRingCat.ofHom C) ≫ terminal.from (Spec (CommRingCat.of (ULift.{u, 0} ℤ))))
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
f : X → Y
h : support f ⊆ U
x : X
⊢ x ∈ support f ↔ x ∈ U \ {x | f x = 0 x}

Tactic:
simp only [mem_support, ne_eq, Pi.zero_apply, Set.mem_sdiff, mem_ofPred_eq, iff_and_self]

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
f : X → Y
h : support f ⊆ U
x : X
⊢ ¬f x = 0 → x ∈ U
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
z : X
t₁ t₂ : Set X
a : X
hf : (∀ (x : X), ¬f x = 0 → x ∈ U) ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite
hg : (∀ (x : X), ¬g x = 0 → x ∈ U) ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support g).Finite
hz : z ∈ U
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ Function.support g).Finite
ha : (a ∈ t₁ ∧ a ∈ t₂) ∧ ¬f a + g a = 0
⊢ ¬f a = 0 ∨ ¬g a = 0

Tactic:
by_contra! hCon

Goal state after:
case right
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
z : X
t₁ t₂ : Set X
a : X
hf : (∀ (x : X), ¬f x = 0 → x ∈ U) ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite
hg : (∀ (x : X), ¬g x = 0 → x ∈ U) ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support g).Finite
hz : z ∈ U
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ Function.support g).Finite
ha : (a ∈ t₁ ∧ a ∈ t₂) ∧ ¬f a + g a = 0
hCon : f a = 0 ∧ g a = 0
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case refine_1
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
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
⊢ ∀ (i : CategoryTheory.Pairwise ι), D.obj i ≤ UX

Tactic:
subst hVU

Goal state after:
case refine_1
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
hUST : UT ≤ f ⁻¹ᵁ US
UY : Y.Opens
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hUY : UY = g ⁻¹ᵁ iSup VX ⊓ iY ⁻¹ᵁ UT
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
⊢ ∀ (i : CategoryTheory.Pairwise ι), D.obj i ≤ iSup VX
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case refine_2
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
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
⊢ UX ≤ iSup D.obj

Tactic:
subst hVU

Goal state after:
case refine_2
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
hUST : UT ≤ f ⁻¹ᵁ US
UY : Y.Opens
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hUY : UY = g ⁻¹ᵁ iSup VX ⊓ iY ⁻¹ᵁ UT
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
⊢ iSup VX ≤ iSup D.obj
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeSup Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
a : X
ha : (a ∈ t₁ ∧ a ∈ t₂) ∧ ¬D₁ a ⊔ D₂ a = 0
⊢ ¬D₁ a = 0 ∨ ¬D₂ a = 0

Tactic:
by_contra! hCon

Goal state after:
case right
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeSup Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
a : X
ha : (a ∈ t₁ ∧ a ∈ t₂) ∧ ¬D₁ a ⊔ D₂ a = 0
hCon : D₁ a = 0 ∧ D₂ a = 0
⊢ False
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeInf Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
a : X
ha : (a ∈ t₁ ∧ a ∈ t₂) ∧ ¬D₁ a ⊓ D₂ a = 0
⊢ ¬D₁ a = 0 ∨ ¬D₂ a = 0

Tactic:
by_contra! hCon

Goal state after:
case right
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeInf Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
a : X
ha : (a ∈ t₁ ∧ a ∈ t₂) ∧ ¬D₁ a ⊓ D₂ a = 0
hCon : D₁ a = 0 ∧ D₂ a = 0
⊢ False
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this✝² : Algebra ↑R ↑A := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset ↑A
hs : Algebra.adjoin ↑R ↑s = ⊤
W : ↑A → TopologicalSpace.Opens ↥X
hxW : ∀ (t : ↑A), x ∈ W t
f : (t : ↑A) → ToType (X.presheaf.obj (Opposite.op (W t)))
hf : ∀ (t : ↑A), (ConcreteCategory.hom (X.presheaf.germ (W t) x ⋯)) (f t) = (ConcreteCategory.hom φ) t
H : x ∈ s.inf W ⊓ U
this✝¹ : Algebra ↑R ↑Γ(X, U) := (CommRingCat.Hom.hom φRX).toAlgebra
this✝ : Algebra ↑R ↑(X.presheaf.stalk x) := (CommRingCat.Hom.hom (φRX ≫ X.presheaf.germ U x hxU)).toAlgebra
this : Algebra ↑R ↑(X.presheaf.obj (Opposite.op (s.inf W ⊓ U))) :=
  (CommRingCat.Hom.hom (φRX ≫ X.presheaf.map (homOfLE ⋯).op)).toAlgebra
φ' : ↑A →ₐ[↑R] ↑(X.presheaf.stalk x) :=
  let __src := CommRingCat.Hom.hom φ;
  { toRingHom := __src, commutes' := ⋯ }
ψ : ↑Γ(X, s.inf W ⊓ U) →ₐ[↑R] ↑(X.presheaf.stalk x) :=
  let __src := CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H);
  { toRingHom := __src, commutes' := ⋯ }
⊢ φ'.range ≤ ψ.range

Tactic:
← Algebra.map_top,

Goal state after:
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this✝² : Algebra ↑R ↑A := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset ↑A
hs : Algebra.adjoin ↑R ↑s = ⊤
W : ↑A → TopologicalSpace.Opens ↥X
hxW : ∀ (t : ↑A), x ∈ W t
f : (t : ↑A) → ToType (X.presheaf.obj (Opposite.op (W t)))
hf : ∀ (t : ↑A), (ConcreteCategory.hom (X.presheaf.germ (W t) x ⋯)) (f t) = (ConcreteCategory.hom φ) t
H : x ∈ s.inf W ⊓ U
this✝¹ : Algebra ↑R ↑Γ(X, U) := (CommRingCat.Hom.hom φRX).toAlgebra
this✝ : Algebra ↑R ↑(X.presheaf.stalk x) := (CommRingCat.Hom.hom (φRX ≫ X.presheaf.germ U x hxU)).toAlgebra
this : Algebra ↑R ↑(X.presheaf.obj (Opposite.op (s.inf W ⊓ U))) :=
  (CommRingCat.Hom.hom (φRX ≫ X.presheaf.map (homOfLE ⋯).op)).toAlgebra
φ' : ↑A →ₐ[↑R] ↑(X.presheaf.stalk x) :=
  let __src := CommRingCat.Hom.hom φ;
  { toRingHom := __src, commutes' := ⋯ }
ψ : ↑Γ(X, s.inf W ⊓ U) →ₐ[↑R] ↑(X.presheaf.stalk x) :=
  let __src := CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H);
  { toRingHom := __src, commutes' := ⋯ }
⊢ Subalgebra.map φ' ⊤ ≤ ψ.range
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
g : Y ⟶ Z
⊢ X ⤏ Z

Tactic:
refine Quotient.map (PartialMap.compHom · g) ?_ f
  intro f₁ f₂ ⟨W, hW, hWl, hWr, e⟩
  refine ⟨W, hW, hWl, hWr, ?_⟩
  simp only [PartialMap.restrict_domain, PartialMap.restrict_hom, PartialMap.compHom_domain,
    PartialMap.compHom_hom] at e ⊢
  rw [reassoc_of% e]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
i' : 𝒰.I₀ → I
f : (j : 𝒰.I₀) → i' j ⟶ i
hf : ∀ (j : 𝒰.I₀), IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j)
g : (j : I) →
  j ∈ insert i (Finset.image i' Finset.univ) →
    (IsCofiltered.inf (insert i (Finset.image i' Finset.univ))
        (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ) ⟶
      j) :=
  fun j ↦
    IsCofiltered.infTo (insert i (Finset.image i' Finset.univ))
      (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ)
j : 𝒰.I₀
F : (Precoverage.ZeroHypercover.pullback₁ (D.map (g i ⋯)) 𝒰).X j ⟶
  (Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j :=
  pullback.map (D.map (g i ⋯)) (𝒰.f j) (D.map (f j)) (𝒰.f j) (D.map (g (i' j) ⋯)) (𝟙 (𝒰.X j)) (𝟙 (D.obj i)) ⋯ ⋯
⊢ IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (g i ⋯)) 𝒰).X j)

Tactic:
exact Function.isEmpty F

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: 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
H✝ : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace ↥((opensDiagram D i U).obj j)
H : ((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V = ⊤
⊢ (opensCone D c i U).π.app (Over.mk (𝟙 i)) ⁻¹ᵁ (((D.obj i).isoOfEq ⋯).hom ≫ U.ι) ⁻¹ᵁ V = ⊤

Tactic:
simpa [← Scheme.Hom.comp_preimage, -Scheme.Hom.comp_base]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: 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
⊢ ∃ j fji, D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V

Tactic:
refine ⟨k, fkj₁ ≫ fj₁i, le_antisymm ?_ ?_⟩

Goal state after:
case refine_1
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) ⁻¹ᵁ U ≤ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ V

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