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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
⊢ ∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (⇑f ⁻¹' U)

Tactic:
intro U

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Set ↥Y
⊢ IsOpen U → IsCompact U → IsCompact (⇑f ⁻¹' U)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
⊢ ∀ (U : Set ↥Z), IsOpen U → IsCompact U → IsCompact (⇑(f ≫ g) ⁻¹' U)

Tactic:
intro U

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↥Z
⊢ IsOpen U → IsCompact U → IsCompact (⇑(f ≫ g) ⁻¹' U)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
this : ∀ (U : X.Opens), IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier
⊢ ∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)

Tactic:
intro U

Goal state after:
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
this : ∀ (U : X.Opens), IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier
U : Set ↥X
⊢ ∀ (V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mpr
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
⊢ ∀ (U : X.Opens), IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier

Tactic:
intro U

Goal state after:
case mpr
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
⊢ IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion f
H :
  ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (↑V) e))
⊢ ∀ (U : ↑Z.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) (↑U) (↑V) e))

Tactic:
intro U

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion f
H :
  ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (↑V) e))
U : ↑Z.affineOpens
⊢ ∀ (V : ↑X.affineOpens) (e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) (↑U) (↑V) e))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
⊢ sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
intro U

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
U : ↑X.affineOpens
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
⊢ ∀ (i : ↑X.affineOpens), P (𝟙 X ∣_ ↑i)

Tactic:
intro U

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
U : ↑X.affineOpens
⊢ P (𝟙 X ∣_ ↑U)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : Subsingleton R
⊢ I.height = ⊤

Tactic:
by
  rw [Subsingleton.elim I ⊤, Ideal.height_top]

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

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Z → P (f ≫ g)
hZ : ¬IsAffine Z
⊢ ∀ (i : ↑Z.affineOpens), P ((f ≫ g) ∣_ ↑i)

Tactic:
intro U

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Z → P (f ≫ g)
hZ : ¬IsAffine Z
U : ↑Z.affineOpens
⊢ P ((f ≫ g) ∣_ ↑U)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
this : ∀ {X Y Z : Scheme} {f : X ⟶ Y} {g : Y ⟶ Z}, P (f ≫ g) → IsAffine Z → P f
hZ : ¬IsAffine Z
⊢ ∀ (i : ↑Z.affineOpens), P (f ∣_ g ⁻¹ᵁ ↑i)

Tactic:
intro U

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
this : ∀ {X Y Z : Scheme} {f : X ⟶ Y} {g : Y ⟶ Z}, P (f ≫ g) → IsAffine Z → P f
hZ : ¬IsAffine Z
U : ↑Z.affineOpens
⊢ P (f ∣_ g ⁻¹ᵁ ↑U)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
hZ : IsAffine Z
this : ∀ {X Y : Scheme} {f : X ⟶ Y} {g : Y ⟶ Z}, P (f ≫ g) → IsAffine Y → P f
hY : ¬IsAffine Y
⊢ ∀ (i : ↑Y.affineOpens), P (f ∣_ ↑i)

Tactic:
intro U

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
hZ : IsAffine Z
this : ∀ {X Y : Scheme} {f : X ⟶ Y} {g : Y ⟶ Z}, P (f ≫ g) → IsAffine Y → P f
hY : ¬IsAffine Y
U : ↑Y.affineOpens
⊢ P (f ∣_ ↑U)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
Z : Scheme
hZ : IsAffine Z
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
hY✝ : IsAffine Y
this : ∀ {X : Scheme} {f : X ⟶ Y}, P (f ≫ g) → IsAffine X → P f
hY : ¬IsAffine X
⊢ ∀ (i : ↑X.affineOpens), P ((↑i).ι ≫ f)

Tactic:
intro U

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
Z : Scheme
hZ : IsAffine Z
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
hY✝ : IsAffine Y
this : ∀ {X : Scheme} {f : X ⟶ Y}, P (f ≫ g) → IsAffine X → P f
hY : ¬IsAffine X
U : ↑X.affineOpens
⊢ P ((↑U).ι ≫ f)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsReduced Y
⊢ autoParam (∀ (U : X.Opens), _root_.IsReduced ↑Γ(X, U)) IsReduced.component_reduced._autoParam

Tactic:
intro U

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsReduced Y
U : X.Opens
⊢ _root_.IsReduced ↑Γ(X, U)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case h
X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
this : Finite ↑s
val✝ : Fintype ↑s
hs : S ⊓ ↑U = ⨆ i, ↑↑i
hs₁ : ∀ (i : ↑s), ↑↑i ≤ S
hs₂ : ∀ (i : ↑s), ↑↑i ≤ ↑U
n : ↑s → ℕ
hn : ∀ (i : ↑s) (m : ℕ), n i ≤ m → (((f |_ S) ⋯ ^ (m + n₂) * y₁) |_ ↑↑i) ⋯ = (((f |_ ↑U) ⋯ ^ (m + n₁) * y₂) |_ ↑↑i) ⋯
⊢ ∀ (i : ↑s),
    (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op))
          ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₂) * y₁)) =
      (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op))
          ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (Finset.univ.sup n + n₁) * y₂))

Tactic:
intro i
        -- This unfolds `X.sheaf`
        change (X.presheaf.map _) _ = (X.presheaf.map _) _
        simp only [← CommRingCat.comp_apply, ← Functor.map_comp, ← op_comp]
        apply hn
        exact Finset.le_sup (Finset.mem_univ _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
⊢ autoParam (∀ (U : X.Opens), _root_.IsReduced ↑Γ(X, U)) IsReduced.component_reduced._autoParam

Tactic:
intro U

Goal state after:
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
⊢ _root_.IsReduced ↑Γ(X, U)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
this : ∀ {X Y Z : Scheme} (i : Y ⟶ Z), IsOpenImmersion i → ∀ (f : X ⟶ Y), P f → IsAffine Z → P (f ≫ i)
hZ : ¬IsAffine Z
⊢ ∀ (i_1 : ↑Z.affineOpens), P ((f ≫ i) ∣_ ↑i_1)

Tactic:
intro U

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
this : ∀ {X Y Z : Scheme} (i : Y ⟶ Z), IsOpenImmersion i → ∀ (f : X ⟶ Y), P f → IsAffine Z → P (f ≫ i)
hZ : ¬IsAffine Z
U : ↑Z.affineOpens
⊢ P ((f ≫ i) ∣_ ↑U)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case refine_1.mp
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS✝ : IsClosed S
hT✝ : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝¹ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this✝ : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
this : Nonempty ↥↑({ carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ })
x : ↥X
hS : x ∈ ↑{ carrier := Sᶜ, is_open' := ⋯ }
hT : x ∈ ↑{ carrier := Tᶜ, is_open' := ⋯ }
⊢ x ∈ ↑⊥

Tactic:
rcases h₁ (show x ∈ ⊤ by trivial) with h | h

Goal state after:
case refine_1.mp.inl
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS✝ : IsClosed S
hT✝ : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝¹ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this✝ : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
this : Nonempty ↥↑({ carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ })
x : ↥X
hS : x ∈ ↑{ carrier := Sᶜ, is_open' := ⋯ }
hT : x ∈ ↑{ carrier := Tᶜ, is_open' := ⋯ }
h : x ∈ S
⊢ x ∈ ↑⊥

case refine_1.mp.inr
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS✝ : IsClosed S
hT✝ : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝¹ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this✝ : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
this : Nonempty ↥↑({ carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ })
x : ↥X
hS : x ∈ ↑{ carrier := Sᶜ, is_open' := ⋯ }
hT : x ∈ ↑{ carrier := Tᶜ, is_open' := ⋯ }
h : x ∈ T
⊢ x ∈ ↑⊥
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case component_integral
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
⊢ autoParam (∀ (U : X.Opens) [Nonempty ↥↑U], IsDomain ↑Γ(X, U)) IsIntegral.component_integral._autoParam

Tactic:
intro U

Goal state after:
case component_integral
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
U : X.Opens
⊢ ∀ [Nonempty ↥↑U], IsDomain ↑Γ(X, U)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case component_integral
X Y : Scheme
f : X ⟶ Y
inst✝² : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↥X
⊢ autoParam (∀ (U : X.Opens) [Nonempty ↥↑U], IsDomain ↑Γ(X, U)) IsIntegral.component_integral._autoParam

Tactic:
intro U

Goal state after:
case component_integral
X Y : Scheme
f : X ⟶ Y
inst✝² : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↥X
U : X.Opens
⊢ ∀ [Nonempty ↥↑U], IsDomain ↑Γ(X, U)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ ∀ (i : ↑X.affineOpens), IsClosed (Subtype.val ⁻¹' I.supportSet)

Tactic:
intro U

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ IsClosed (Subtype.val ⁻¹' I.supportSet)
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
⊢ IsOpenMap ⇑f

Tactic:
intro U

Goal state after:
case refine_1
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
⊢ IsOpen U → IsOpen (⇑f '' U)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
this : ∀ {X Y : Scheme} {f : X ⟶ Y}, (∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) → IsAffine Y → P f
hY : ¬IsAffine Y
⊢ ∀ (i : ↑Y.affineOpens), P (f ∣_ ↑i)

Tactic:
intro U

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
this : ∀ {X Y : Scheme} {f : X ⟶ Y}, (∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) → IsAffine Y → P f
hY : ¬IsAffine Y
U : ↑Y.affineOpens
⊢ P (f ∣_ ↑U)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ I.support = ⊥ ↔ I = ⊤

Tactic:
by
  refine ⟨fun H ↦ top_le_iff.mp fun U ↦ ?_, by simp +contextual⟩
  have := (U.2.fromSpec_image_zeroLocus _).trans_subset
    ((zeroLocus_inter_subset_supportSet I U).trans H.le)
  simp only [Set.subset_empty_iff, Set.image_eq_empty, Closeds.coe_bot] at this
  simp [PrimeSpectrum.zeroLocus_empty_iff_eq_top.mp this]

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

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this : ∀ {X : Scheme} {f : X ⟶ Y}, (∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) → IsAffine X → P f
hX : ¬IsAffine X
⊢ ∀ (i : ↑X.affineOpens), P ((↑i).ι ≫ f)

Tactic:
intro U

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this : ∀ {X : Scheme} {f : X ⟶ Y}, (∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) → IsAffine X → P f
hX : ¬IsAffine X
U : ↑X.affineOpens
⊢ P ((↑U).ι ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑f
U : ↥X → Scheme
i : (x : ↥X) → U x ⟶ X
x✝ : ∀ (x : ↥X), IsOpenImmersion (i x)
hxi : ∀ (x : ↥X), x ∈ Scheme.Hom.opensRange (i x)
hi : ∀ (x : ↥X), IsOpenImmersion (i x ≫ f)
⊢ { I₀ := ↥X, X := U, f := i }.presieve₀ ∈ Scheme.jointlySurjectivePrecoverage.coverings X

Tactic:
by simpa using show ∀ x, ∃ j y, i j y = x from (⟨_, hxi ·⟩)

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

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
I J : X.IdealSheafData
H : I.ideal ⟨⊤, ⋯⟩ ≤ J.ideal ⟨⊤, ⋯⟩
⊢ I ≤ J

Tactic:
intro U

Goal state after:
X : Scheme
inst✝ : IsAffine X
I J : X.IdealSheafData
H : I.ideal ⟨⊤, ⋯⟩ ≤ J.ideal ⟨⊤, ⋯⟩
U : ↑X.affineOpens
⊢ I.ideal U ≤ J.ideal U
Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ isomorphisms Scheme f✝ ↔ (IsOpenImmersion ⊓ @Surjective) f✝

Tactic:
rw [isomorphisms.iff, isIso_iff_isOpenImmersion_and_surjective]

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ IsOpenImmersion f✝ ∧ Surjective f✝ ↔ (IsOpenImmersion ⊓ @Surjective) f✝
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case refine_2
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
f : ↑Γ(X, ↑V)
hU : U = X.affineBasicOpen f
this✝¹ : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯).toAlgebra
this✝ : Algebra ↑Γ(X, ↑V) ↑Γ(X, ↑U) := (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
this : IsLocalization.Away f ↑Γ(X, ↑U)
⊢ RingHom.ker (Ideal.Quotient.mk (I.ideal U)) ≤
    Ideal.map (algebraMap ↑Γ(X, ↑V) ↑Γ(X, ↑U)) (RingHom.ker (Ideal.Quotient.mk (I.ideal V)))

Tactic:
simp only [Ideal.mk_ker, RingHom.algebraMap_toAlgebra, I.map_ideal', le_refl]

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

Goal state before:
pp: case refine_1
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U : ↑Y.affineOpens
⊢ ∀ (U : ↑Y.affineOpens) (f_1 : ↑Γ(Y, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)) (RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) =
      RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen f_1)))

Tactic:
intro U

Goal state after:
case refine_1
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
⊢ ∀ (f_1 : ↑Γ(Y, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)) (RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) =
      RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen f_1)))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
Z : LocallyRingedSpace
g : Y ⟶ Z
x : ↑X.toTopCat
⊢ CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalRing.ResidueField.map
          (CommRingCat.Hom.hom (Hom.stalkMap g ((ConcreteCategory.hom f.base) x) ≫ Hom.stalkMap f x)))) =
    CommRingCat.Hom.hom
      (CommRingCat.ofHom
          (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap g ((ConcreteCategory.hom f.base) x)))) ≫
        CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x))))

Tactic:
apply IsLocalRing.ResidueField.map_comp (Hom.stalkMap g (f.base x)).hom (Hom.stalkMap f x).hom

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x✝¹ : ↑Γ(X, ↑V)
hx : x✝¹ ∈ I.ideal V
x : ↥↑(↑U ⊓ ↑V)
x✝ : x ∈ ⊤
⊢ x ∈ (↑U ⊓ ↑V).ι ⁻¹ᵁ ↑V

Tactic:
by simpa using x.2.2

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

Goal state before:
pp: case inr
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
h✝ : Nonempty 𝒰.I₀
⊢ ∀ (U : ↑Y.affineOpens), (⋃ i, ↑(ker (𝒰.f i ≫ f)).support) ∩ ↑↑U = ↑f.ker.support ∩ ↑↑U

Tactic:
intro U

Goal state after:
case inr
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
h✝ : Nonempty 𝒰.I₀
U : ↑Y.affineOpens
⊢ (⋃ i, ↑(ker (𝒰.f i ≫ f)).support) ∩ ↑↑U = ↑f.ker.support ∩ ↑↑U
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
⊢ ∀ (U : Z.Opens), IsAffineOpen U → IsAffineOpen ((f ≫ g) ⁻¹ᵁ U)

Tactic:
intro U

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
U : Z.Opens
⊢ IsAffineOpen U → IsAffineOpen ((f ≫ g) ⁻¹ᵁ U)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
r : ↑Γ(X, ⊤)
⊢ ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen ((X.basicOpen r).ι ⁻¹ᵁ U)

Tactic:
intro U

Goal state after:
X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
r : ↑Γ(X, ⊤)
U : X.Opens
⊢ IsAffineOpen U → IsAffineOpen ((X.basicOpen r).ι ⁻¹ᵁ U)