mathlib-initiative/mathlib-tactics huggingface dataset:
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:
]

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
⊢ ∀ (i : ↑X.affineOpens), P ((↑i).ι ≫ f)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s : ToType (X.presheaf.obj (op U))
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) (s ^ n) = (CommRingCat.Hom.hom (X.presheaf.germ U x hxU)) 0
V : Opens ↥X
hxV : x ∈ V
iU iV : V ⟶ U
e' : (ConcreteCategory.hom (X.presheaf.map iU.op)) s = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsReduced Y
U : X.Opens
⊢ _root_.IsReduced ↑Γ(X, f ⁻¹ᵁ f ''ᵁ U)

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsReduced Y
U : X.Opens
⊢ _root_.IsReduced ↑Γ(X, f ⁻¹ᵁ 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
U : ↑X.affineOpens
H : P (((↑U).ι ≫ f) ≫ g)
⊢ P ((↑U).ι ≫ f)

Tactic:
]

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
H : P (((↑U).ι ≫ f) ≫ g)
⊢ P ((↑U).ι ≫ f)
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
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
Y : Scheme
g : Y ⟶ Z
hY✝ : IsAffine Y
X : Scheme
f : X ⟶ Y
h : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ≫ g)))
hY : IsAffine X
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
]

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
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
Y : Scheme
g : Y ⟶ Z
hY✝ : IsAffine Y
X : Scheme
f : X ⟶ Y
h : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ≫ g)))
hY : IsAffine X
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
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.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : P g
⊢ P (pullback.fst f g)

Tactic:
]

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.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : P g
⊢ P (pullback.fst f g)
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.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this✝ : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : P g
this : ∀ ⦃Y : Scheme⦄ (g : Y ⟶ S), P g → IsAffine Y → P (pullback.fst f g)
hX : ¬IsAffine Y
⊢ ∀ (i : (Scheme.Pullback.openCoverOfRight Y.affineCover f g).I₀),
    P ((Scheme.Pullback.openCoverOfRight Y.affineCover f g).f i ≫ pullback.fst f g)

Tactic:
]

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.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this✝ : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : P g
this : ∀ ⦃Y : Scheme⦄ (g : Y ⟶ S), P g → IsAffine Y → P (pullback.fst f g)
hX : ¬IsAffine Y
⊢ ∀ (i : (Scheme.Pullback.openCoverOfRight Y.affineCover f g).I₀),
    P ((Scheme.Pullback.openCoverOfRight Y.affineCover f g).f i ≫ pullback.fst f g)
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.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
Y : Scheme
g : Y ⟶ S
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hX : IsAffine Y
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst f g)))

Tactic:
]

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.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
Y : Scheme
g : Y ⟶ S
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hX : IsAffine Y
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst f g)))
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 : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ ∀ (i : ↑Us), P ((V i).ι ≫ f ≫ U.ι)

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 : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ iSup V = ⊤

Tactic:
]

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 : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ ∀ (i : ↑Us), P ((V i).ι ≫ f ≫ U.ι)

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 : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ iSup V = ⊤
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: P : (X : Scheme) → ↥X → Prop
h₁ : ∀ (R : CommRingCat) (x : ↥(Spec R)), P (Spec R) x
h₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X), P X x → P Y (f x)
X : Scheme
x : ↥X
y : ↥(X.affineCover.X (Scheme.Cover.idx X.affineCover x))
e : (X.affineCover.f (Scheme.Cover.idx X.affineCover x)) y = x
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
hX : IsReduced X
U : X.Opens
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
x : ↥X
hx : x ∈ U
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = 0

Tactic:
]

Goal state after:
X : Scheme
hX : IsReduced X
U : X.Opens
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
x : ↥X
hx : x ∈ U
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₁
X✝ X : Scheme
U : X.Opens
H✝ :
  ∀ (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V),
        ∃ x,
          ∀ [hX : IsReduced X] (s : ↑Γ(X, V)),
            X.basicOpen s = ⊥ → ∀ (x : ↥X) (hx : x ∈ V), (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) s = 0
hX : IsReduced X
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
x : ↥X
hx✝ : x ∈ U
V : X.Opens
hx : ↑⟨x, hx✝⟩ ∈ V
i : V ⟶ U
H :
  V ⊓ ⊥ = ⊥ →
    ∀ (x : ↥X) (hx : x ∈ V),
      (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) ((ConcreteCategory.hom (X.presheaf.map i.op)) s) = 0
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx✝)) s = 0

Tactic:
]

Goal state after:
case h₁
X✝ X : Scheme
U : X.Opens
H✝ :
  ∀ (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V),
        ∃ x,
          ∀ [hX : IsReduced X] (s : ↑Γ(X, V)),
            X.basicOpen s = ⊥ → ∀ (x : ↥X) (hx : x ∈ V), (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) s = 0
hX : IsReduced X
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
x : ↥X
hx✝ : x ∈ U
V : X.Opens
hx : ↑⟨x, hx✝⟩ ∈ V
i : V ⟶ U
H :
  V ⊓ ⊥ = ⊥ →
    ∀ (x : ↥X) (hx : x ∈ V),
      (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) ((ConcreteCategory.hom (X.presheaf.map i.op)) s) = 0
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx✝)) s = 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₁
X✝ X : Scheme
U : X.Opens
H✝ :
  ∀ (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V),
        ∃ x,
          ∀ [hX : IsReduced X] (s : ↑Γ(X, V)),
            X.basicOpen s = ⊥ → ∀ (x : ↥X) (hx : x ∈ V), (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) s = 0
hX : IsReduced X
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
x : ↥X
hx✝ : x ∈ U
V : X.Opens
hx : ↑⟨x, hx✝⟩ ∈ V
i : V ⟶ U
H : (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) ((ConcreteCategory.hom (X.presheaf.map i.op)) s) = 0
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) ((ConcreteCategory.hom (X.sheaf.presheaf.map i.op)) s) = 0

Tactic:
]

Goal state after:
case h₁
X✝ X : Scheme
U : X.Opens
H✝ :
  ∀ (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V),
        ∃ x,
          ∀ [hX : IsReduced X] (s : ↑Γ(X, V)),
            X.basicOpen s = ⊥ → ∀ (x : ↥X) (hx : x ∈ V), (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) s = 0
hX : IsReduced X
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
x : ↥X
hx✝ : x ∈ U
V : X.Opens
hx : ↑⟨x, hx✝⟩ ∈ V
i : V ⟶ U
H : (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) ((ConcreteCategory.hom (X.presheaf.map i.op)) s) = 0
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) ((ConcreteCategory.hom (X.sheaf.presheaf.map i.op)) s) = 0
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 : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq✝ : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
s : ↑Us
f' : ↑(V s) ⟶ ↑(U.ι ⁻¹ᵁ ↑s) := f ∣_ U.ι ⁻¹ᵁ ↑s
hf' : P f'
e : ↑(U.ι ⁻¹ᵁ ↑s) ≅ ↑↑s := IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ ↑s).ι ≫ U.ι) (↑s).ι ⋯
heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s).ι
⊢ P ((f' ≫ e.hom) ≫ (↑s).ι)

Tactic:
]

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 : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq✝ : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
s : ↑Us
f' : ↑(V s) ⟶ ↑(U.ι ⁻¹ᵁ ↑s) := f ∣_ U.ι ⁻¹ᵁ ↑s
hf' : P f'
e : ↑(U.ι ⁻¹ᵁ ↑s) ≅ ↑↑s := IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ ↑s).ι ≫ U.ι) (↑s).ι ⋯
heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s).ι
⊢ P ((f' ≫ e.hom) ≫ (↑s).ι)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : ↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f)),
    X.basicOpen s = ⊥ →
      ∀ (x : ↥X) (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
        (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx)) s = 0
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
⊢ f ⁻¹ᵁ ⊥ = ⊥

Tactic:
]

Goal state after:
case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : ↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f)),
    X.basicOpen s = ⊥ →
      ∀ (x : ↥X) (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
        (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx)) s = 0
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
⊢ f ⁻¹ᵁ ⊥ = ⊥
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
H✝ :
  (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯))
      ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) =
    0
this : IsReduced X
H :
  (ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
      ((ConcreteCategory.hom (Y.presheaf.germ { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ } (f x) ⋯))
        s) =
    0
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) (f x) ⋯)) s = 0

Tactic:
]

Goal state after:
case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
H✝ :
  (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯))
      ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) =
    0
this : IsReduced X
H :
  (ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
      ((ConcreteCategory.hom (Y.presheaf.germ { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ } (f x) ⋯))
        s) =
    0
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) (f x) ⋯)) s = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr.refine_1
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 : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq✝ : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
s : ↑Us
f' : ↑(V s) ⟶ ↑(U.ι ⁻¹ᵁ ↑s) := f ∣_ U.ι ⁻¹ᵁ ↑s
hf' : P f'
e : ↑(U.ι ⁻¹ᵁ ↑s) ≅ ↑↑s := IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ ↑s).ι ≫ U.ι) (↑s).ι ⋯
heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s).ι
⊢ P f'

Tactic:
]

Goal state after:
case inr.refine_1
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 : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq✝ : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
s : ↑Us
f' : ↑(V s) ⟶ ↑(U.ι ⁻¹ᵁ ↑s) := f ∣_ U.ι ⁻¹ᵁ ↑s
hf' : P f'
e : ↑(U.ι ⁻¹ᵁ ↑s) ≅ ↑↑s := IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ ↑s).ι ≫ U.ι) (↑s).ι ⋯
heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s).ι
⊢ P f'
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case e_supportSet
X : Scheme
i : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen✝¹ :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (i U) = i (X.affineBasicOpen f)
s : Set ↥X
hs : s = ⋂ U, X.zeroLocus ↑(i U)
t : Set ↥X
map_ideal_basicOpen✝ :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
        ({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s,
              supportSet_eq_iInter_zeroLocus := hs }.ideal
          U) =
      { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s,
            supportSet_eq_iInter_zeroLocus := hs }.ideal
        (X.affineBasicOpen f)
ht :
  t =
    ⋂ U,
      X.zeroLocus
        ↑({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s,
                supportSet_eq_iInter_zeroLocus := hs }.ideal
            U)
⊢ ⋂ U, X.zeroLocus ↑(i U) =
    ⋂ U,
      X.zeroLocus
        ↑({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s,
                supportSet_eq_iInter_zeroLocus := hs }.ideal
            U)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
H✝ :
  (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯))
      ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) =
    0
this : IsReduced X
H :
  (ConcreteCategory.hom (𝟙 (Y.presheaf.stalk (f x))))
      ((ConcreteCategory.hom (Y.presheaf.germ { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ } (f x) ⋯))
        s) =
    0
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) (f x) ⋯)) s = 0

Tactic:
]

Goal state after:
case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
H✝ :
  (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯))
      ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) =
    0
this : IsReduced X
H :
  (ConcreteCategory.hom (𝟙 (Y.presheaf.stalk (f x))))
      ((ConcreteCategory.hom (Y.presheaf.germ { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ } (f x) ⋯))
        s) =
    0
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) (f x) ⋯)) s = 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
hs : IsNilpotent ((ConcreteCategory.hom (Scheme.ΓSpecIso R).hom) s)
x : ↥(Spec R)
hx : x ∈ ⊤
⊢ (ConcreteCategory.hom ((Spec R).sheaf.presheaf.germ ⊤ x hx)) s = 0

Tactic:
]

Goal state after:
case h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
hs : IsNilpotent ((ConcreteCategory.hom (Scheme.ΓSpecIso R).hom) s)
x : ↥(Spec R)
hx : x ∈ ⊤
⊢ (ConcreteCategory.hom ((Spec R).sheaf.presheaf.germ ⊤ x hx)) s = 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
x : ↥(Spec R)
hx : x ∈ ⊤
hs : s = 0
⊢ (ConcreteCategory.hom ((Spec R).sheaf.presheaf.germ ⊤ x hx)) s = 0

Tactic:
]

Goal state after:
case h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
x : ↥(Spec R)
hx : x ∈ ⊤
hs : s = 0
⊢ (ConcreteCategory.hom ((Spec R).sheaf.presheaf.germ ⊤ x hx)) s = 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
x : ↥(Spec R)
hx : x ∈ ⊤
hs : s = 0
⊢ 0 = 0

Tactic:
]

Goal state after: