awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
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_1 : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
x : ↥(Spec S)
hX : IsAffine.{u} (Spec S)
f : Spec S ⟶ Spec R
hf : P f
obtain : ∀ (φ : R ⟶ S) (hf : P (Spec.map φ)), Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
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
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
x : ↥(Spec S)
hX : IsAffine.{u} (Spec S)
φ : R ⟶ S
hf : P (Spec.map φ)
rw :
  Q' (R := (↑(CommRingCat.of (Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) x).asIdeal)) : Type u))
    (S := (↑(CommRingCat.of (Localization.AtPrime x.asIdeal)) : Type u))
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) x).asIdeal x.asIdeal
          (CommRingCat.Hom.hom φ) ⋯)))
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))

Tactic:
rw [hQ'.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso φ _)]

Premises used: AlgebraicGeometry.Scheme.arrowStalkMapSpecIso, RingHom.RespectsIso.arrow_mk_iso_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
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
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
x : ↥(Spec S)
hX : IsAffine.{u} (Spec S)
φ : R ⟶ S
hf : P (Spec.map φ)
⊢ Q (CommRingCat.Hom.hom φ)

Tactic:
rw [Spec_iff (P := P)] at hf

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
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
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
x : ↥(Spec S)
hX : IsAffine.{u} (Spec S)
φ : R ⟶ S
hf : Q (CommRingCat.Hom.hom φ)
⊢ Q' (R := (↑(CommRingCat.of (Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) x).asIdeal)) : Type u))
    (S := (↑(CommRingCat.of (Localization.AtPrime x.asIdeal)) : Type u))
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) x).asIdeal x.asIdeal
          (CommRingCat.Hom.hom φ) ⋯)))

Tactic:
apply hQ _ hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
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 :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
stalkMap_of_respectsIso (HasRingHomProperty.isLocal_ringHomProperty P).respectsIso hQ hf x

Premises used: AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty, AlgebraicGeometry.HasRingHomProperty.stalkMap_of_respectsIso, RingHom.PropertyIsLocal.respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
P' : MorphismProperty Scheme
Q' : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
h : ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] (f : R →+* S), Q f ↔ Q' f
h₁ : ∀ ⦃f Y : Scheme.{u}⦄ (f_1 : f ⟶ Y), P f_1 ↔ P' f_1
⊢ P = P'

Tactic:
ext f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
P' : MorphismProperty Scheme
Q' : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
h : ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] (f : R →+* S), Q f ↔ Q' f
f Y : Scheme
f_1 : f ⟶ Y
h₁ :
  (∀ (U : (↑Y.affineOpens : Type u)) (V : (↑f.affineOpens : Type u)) (e : (↑V : f.Opens) ≤ f_1 ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f_1 (↑U : Y.Opens) (↑V : f.Opens) e))) ↔
    ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑f.affineOpens : Type u)) (e : (↑V : f.Opens) ≤ f_1 ⁻¹ᵁ (↑U : Y.Opens)),
      Q' (CommRingCat.Hom.hom (Scheme.Hom.appLE f_1 (↑U : Y.Opens) (↑V : f.Opens) e))
⊢ P f_1 ↔ P' f_1

Tactic:
rw [HasRingHomProperty.eq_affineLocally (P := P), HasRingHomProperty.eq_affineLocally (P := P'),
    affineLocally_iff_affineOpens_le, affineLocally_iff_affineOpens_le]

Premises used: AlgebraicGeometry.affineLocally_iff_affineOpens_le, AlgebraicGeometry.HasRingHomProperty.eq_affineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
P' : MorphismProperty Scheme
Q' : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
h : ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] (f : R →+* S), Q f ↔ Q' f
f Y : Scheme
f_1 : f ⟶ Y
⊢ (∀ (U : (↑Y.affineOpens : Type u)) (V : (↑f.affineOpens : Type u)) (e : (↑V : f.Opens) ≤ f_1 ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f_1 (↑U : Y.Opens) (↑V : f.Opens) e))) ↔
    ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑f.affineOpens : Type u)) (e : (↑V : f.Opens) ≤ f_1 ⁻¹ᵁ (↑U : Y.Opens)),
      Q' (CommRingCat.Hom.hom (Scheme.Hom.appLE f_1 (↑U : Y.Opens) (↑V : f.Opens) e))

Tactic:
simp only [h]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsIso f
⊢ Scheme.Hom.ker f = ⊥

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
rw : DenseRange (X := ↥S) (α := ↥X) ⇑f
rw₁ : Dense (X := ↥S) (Set.range (ι := ↥X) ⇑f)
rw₂ : Eq (α := Set ↥S) (closure (Set.range (ι := ↥X) ⇑f)) Set.univ
rw₃ : (↑(Scheme.Hom.ker f).support : Set ↥S) = Set.univ
rw₄ : (↑(Scheme.IdealSheafData.support ⊥) : Set ↥S) = Set.univ
rw₅ : (↑⊤ : Set ↥S) = Set.univ
rw₆ rw₇ : Eq.{u_1 + 1} (α := Set ↥S) Set.univ Set.univ
⊢ IsDominant f

Tactic:
rw [isDominant_iff, DenseRange, dense_iff_closure_eq, ← Scheme.Hom.support_ker,
    f.ker_eq_bot, Scheme.IdealSheafData.support_bot, TopologicalSpace.Closeds.coe_top]

Premises used: dense_iff_closure_eq, TopologicalSpace.Closeds.coe_top, AlgebraicGeometry.Scheme.Hom.ker_eq_bot, AlgebraicGeometry.isDominant_iff, DenseRange, AlgebraicGeometry.Scheme.Hom.support_ker, AlgebraicGeometry.Scheme.IdealSheafData.support_bot
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y Z S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSchemeTheoreticallyDominant f
inst_1 : IsSchemeTheoreticallyDominant g
rw : Scheme.Hom.ker (f ≫ g) = ⊥
rw₁ : (Scheme.Hom.ker f).map g = ⊥
rw₂ : Scheme.IdealSheafData.map ⊥ g = ⊥
rw₃ : Scheme.Hom.ker g = ⊥
rw₄ rw₅ : Eq.{u_1 + 1} (α := Z.IdealSheafData) ⊥ ⊥
⊢ IsSchemeTheoreticallyDominant (f ≫ g)

Tactic:
rw [isSchemeTheoreticallyDominant_iff, Scheme.Hom.ker_comp, f.ker_eq_bot,
    Scheme.IdealSheafData.map_bot, g.ker_eq_bot]

Premises used: AlgebraicGeometry.isSchemeTheoreticallyDominant_iff, AlgebraicGeometry.Scheme.Hom.ker_eq_bot, AlgebraicGeometry.Scheme.Hom.ker_comp, AlgebraicGeometry.Scheme.IdealSheafData.map_bot
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsDominant f
inst_1 : IsReduced Y
rw : Set.range (ι := ↥X) ⇑f ⊆ (↑(Scheme.Hom.ker f).support : Set ↥Y)
⊢ IsSchemeTheoreticallyDominant f

Tactic:
rw [isSchemeTheoreticallyDominant_iff, ← Scheme.IdealSheafData.support_eq_top_iff,
    ← SetLike.coe_injective.eq_iff, TopologicalSpace.Closeds.coe_top, ← Set.univ_subset_iff,
    ← f.denseRange.closure_eq, f.ker.support.isClosed.closure_subset_iff]

Premises used: Set.univ_subset_iff, AlgebraicGeometry.Scheme.Hom.denseRange, AlgebraicGeometry.Scheme.IdealSheafData.support, TopologicalSpace.Closeds.isClosed, AlgebraicGeometry.isSchemeTheoreticallyDominant_iff, Function.Injective.eq_iff, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff, AlgebraicGeometry.Scheme.Hom.ker, Dense.closure_eq, SetLike.coe_injective, IsClosed.closure_subset_iff, TopologicalSpace.Closeds.coe_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsDominant f
inst_1 : IsReduced Y
⊢ Set.range (ι := ↥X) ⇑f ⊆ (↑(Scheme.Hom.ker f).support : Set ↥Y)

Tactic:
f.range_subset_ker_support

Premises used: AlgebraicGeometry.Scheme.Hom.range_subset_ker_support
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsDominant f
inst_1 : IsReduced Y
⊢ Set.range (ι := ↥X) ⇑f ⊆ (↑(Scheme.Hom.ker f).support : Set ↥Y)

Tactic:
exact f.range_subset_ker_support

Premises used: AlgebraicGeometry.Scheme.Hom.range_subset_ker_support
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : IsReduced Y
⊢ IsSchemeTheoreticallyDominant f ↔ IsDominant f

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ .of_isDominant _⟩

Premises used: inferInstance, AlgebraicGeometry.IsSchemeTheoreticallyDominant.of_isDominant, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
U : Y.Opens
inr :
  ∀
    (this :
      ∀ (U : Y.Opens) (hU : IsAffineOpen U),
        Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (app f U)) :
            (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1)))
    (hU : ¬IsAffineOpen U),
    Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U)) :
        (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
wlog :
  ∀ (U : Y.Opens) (hU : IsAffineOpen U),
    Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U)) :
        (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
⊢ Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (app f U)) :
      (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))

Tactic:
wlog hU : IsAffineOpen U generalizing U

Premises used: AlgebraicGeometry.IsAffineOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
U : Y.Opens
hU : IsAffineOpen U
rw : IdealSheafData.ideal ⊥ (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) = ⊥
⊢ Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (app f U)) :
      (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))

Tactic:
rw [RingHom.injective_iff_ker_eq_bot, ← f.ker_apply ⟨U, hU⟩, f.ker_eq_bot]

Premises used: AlgebraicGeometry.Scheme.Hom.ker_apply, Subtype.mk, AlgebraicGeometry.Scheme.Hom.ker_eq_bot, RingHom.injective_iff_ker_eq_bot
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
U : Y.Opens
hU : IsAffineOpen U
⊢ IdealSheafData.ideal ⊥ (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) = ⊥

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
U : Y.Opens
this :
  ∀ (U : Y.Opens) (hU : IsAffineOpen U),
    Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U)) :
        (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
hU : ¬IsAffineOpen U
inr :
  ∀ (a : (↑Γ(Y, U) : Type u_1)),
    Eq (α := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (app f U) :
              (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
            a :
          (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
        (0 : (↑Γ(X, f ⁻¹ᵁ U) : Type u_1)) →
      a = 0
⊢ Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (app f U)) :
      (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
U : Y.Opens
this :
  ∀ (U : Y.Opens) (hU : IsAffineOpen U),
    Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U)) :
        (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
hU : ¬IsAffineOpen U
s : (↑Γ(Y, U) : Type u_1)
hs :
  Eq (α := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U) :
          (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
        s :
      (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (0 : (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
⊢ s = 0

Tactic:
Y.IsSheaf.section_ext fun x hx ↦ ?_

Premises used: TopCat.Presheaf.IsSheaf.section_ext, AlgebraicGeometry.SheafedSpace.IsSheaf, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
U : Y.Opens
this :
  ∀ (U : Y.Opens) (hU : IsAffineOpen U),
    Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U)) :
        (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
hU : ¬IsAffineOpen U
s : (↑Γ(Y, U) : Type u_1)
hs :
  Eq (α := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U) :
          (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
        s :
      (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (0 : (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
inr :
  ∀ (x : ↥Y) (hx : x ∈ Opposite.unop (Opposite.op U)),
    ∃ (V : TopologicalSpace.Opens ↥Y) (hV : V ≤ Opposite.unop (Opposite.op U)),
      x ∈ V ∧
        Eq (α := (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (Y.presheaf.map (homOfLE hV).op) :
                (a : (↑(Y.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op U)))) : Type u_1)) →
                  (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
              s :
            (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (Y.presheaf.map (homOfLE hV).op) :
                (a : (↑(Y.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op U)))) : Type u_1)) →
                  (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
              0 :
            (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
⊢ s = 0

Tactic:
refine Y.IsSheaf.section_ext fun x hx ↦ ?_

Premises used: TopCat.Presheaf.IsSheaf.section_ext, AlgebraicGeometry.SheafedSpace.IsSheaf, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
U : Y.Opens
this :
  ∀ (U : Y.Opens) (hU : IsAffineOpen U),
    Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U)) :
        (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
hU : ¬IsAffineOpen U
s : (↑Γ(Y, U) : Type u_1)
hs :
  Eq (α := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U) :
          (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
        s :
      (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (0 : (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
x : ↥Y
hx : x ∈ Opposite.unop (Opposite.op U)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : x ∈ (↑V : Set ↥Y)
hVU : V ≤ U
⊢ ∃ (V : TopologicalSpace.Opens ↥Y) (hV : V ≤ Opposite.unop (Opposite.op U)),
    x ∈ V ∧
      Eq (α := (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Y.presheaf.map (homOfLE hV).op) :
              (a : (↑(Y.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op U)))) : Type u_1)) →
                (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
            s :
          (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Y.presheaf.map (homOfLE hV).op) :
              (a : (↑(Y.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op U)))) : Type u_1)) →
                (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
            0 :
          (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))

Tactic:
⟨V, hVU, hxV, this V hV ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
U : Y.Opens
this :
  ∀ (U : Y.Opens) (hU : IsAffineOpen U),
    Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U)) :
        (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
hU : ¬IsAffineOpen U
s : (↑Γ(Y, U) : Type u_1)
hs :
  Eq (α := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U) :
          (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
        s :
      (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (0 : (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
x : ↥Y
hx : x ∈ Opposite.unop (Opposite.op U)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : x ∈ (↑V : Set ↥Y)
hVU : V ≤ U
⊢ Eq (α := (↑Γ(X, f ⁻¹ᵁ V) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier)
            (app f (Opposite.unop (Opposite.op U)) ≫
              X.presheaf.map ((TopologicalSpace.Opens.map f.base).map (homOfLE hVU).op.unop).op) :
          (a : (↑(Y.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op U)))) : Type u_1)) →
            (↑Γ(X, f ⁻¹ᵁ V) : Type u_1))
        s :
      (↑Γ(X, f ⁻¹ᵁ V) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f V) :
          (a : (↑Γ(Y, V) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Y.presheaf.map (homOfLE hVU).op) :
              (a : (↑(Y.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op U)))) : Type u_1)) →
                (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
            0 :
          (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1)) :
      (↑Γ(X, f ⁻¹ᵁ V) : Type u_1))

Tactic:
simp [hs]