awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
rw : Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) (⇑hU.fromSpec ⁻¹' X.zeroLocus s) = X.zeroLocus s ∩ (↑U : Set ↥X)
rw₁ : X.zeroLocus s ∩ Set.range (ι := ↥(Spec Γ(X, U))) ⇑hU.fromSpec = X.zeroLocus s ∩ (↑U : Set ↥X)
rw₂ rw₃ : X.zeroLocus s ∩ (↑U : Set ↥X) = X.zeroLocus s ∩ (↑U : Set ↥X)
⊢ Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) (PrimeSpectrum.zeroLocus s) = X.zeroLocus s ∩ (↑U : Set ↥X)

Tactic:
rw [← hU.fromSpec_preimage_zeroLocus, Set.image_preimage_eq_inter_range, range_fromSpec]

Premises used: AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus, Set.image_preimage_eq_inter_range, AlgebraicGeometry.IsAffineOpen.range_fromSpec
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
I J : Ideal (↑Γ(X, U) : Type u)
this :
  Eq (α := Set (↑U.carrier : Type u)) (U.carrier ↓∩ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)))
    (U.carrier ↓∩ (X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))))
h :
  ∀ (x : ↥X),
    x ∈ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)) ↔
      x ∈ X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))
⊢ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)) =
    X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
I J : Ideal (↑Γ(X, U) : Type u)
this :
  Eq (α := Set (↑U.carrier : Type u)) (U.carrier ↓∩ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)))
    (U.carrier ↓∩ (X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))))
x : ↥X
pos :
  ∀ (hxU : x ∈ U),
    x ∈ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)) ↔
      x ∈ X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))
neg :
  ∀ (hxU : x ∉ U),
    x ∈ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)) ↔
      x ∈ X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))
⊢ x ∈ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)) ↔
    x ∈ X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))

Tactic:
by_cases hxU : x ∈ U
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
I J : Ideal (↑Γ(X, U) : Type u)
this :
  Eq (α := Set (↑U.carrier : Type u)) (U.carrier ↓∩ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)))
    (U.carrier ↓∩ (X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))))
x : ↥X
hxU : x ∈ U
⊢ x ∈ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)) ↔
    x ∈ X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))

Tactic:
simpa [hxU] using congr(⟨x, hxU⟩ ∈ $this)
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
I J : Ideal (↑Γ(X, U) : Type u)
this :
  Eq (α := Set (↑U.carrier : Type u)) (U.carrier ↓∩ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)))
    (U.carrier ↓∩ (X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))))
x : ↥X
hxU : x ∉ U
⊢ x ∈ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)) ↔
    x ∈ X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))

Tactic:
simp only [Submodule.coe_inf, Set.mem_union,
        codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) (I ∩ J)) hxU,
        codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) I) hxU, true_or]

Premises used: Set.mem_union, codisjoint_iff_compl_le_left, true_or, Inter.inter, Submodule.coe_inf, SetLike.coe, Iff.mp, AlgebraicGeometry.Scheme.codisjoint_zeroLocus
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
I J : Ideal (↑Γ(X, U) : Type u)
suffices :
  Eq (α := Set (↑U.carrier : Type u)) (U.carrier ↓∩ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)))
    (U.carrier ↓∩ (X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))))
⊢ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)) =
    X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))

Tactic:
suffices U.1 ↓∩ (X.zeroLocus (U := U) ↑(I ⊓ J)) =
      U.1 ↓∩ (X.zeroLocus (U := U) I ∪ X.zeroLocus (U := U) J) by
    ext x
    by_cases hxU : x ∈ U
    · simpa [hxU] using congr(⟨x, hxU⟩ ∈ $this)
    · simp only [Submodule.coe_inf, Set.mem_union,
        codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) (I ∩ J)) hxU,
        codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) I) hxU, true_or]
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
I J : Ideal (↑Γ(X, U) : Type u)
⊢ Eq (α := Set (↑U.carrier : Type u)) (U.carrier ↓∩ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)))
    (U.carrier ↓∩ (X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))))

Tactic:
simp only [← U.toSpecΓ_preimage_zeroLocus, PrimeSpectrum.zeroLocus_inf I J,
    Set.preimage_union]

Premises used: Set.preimage_union, PrimeSpectrum.zeroLocus_inf, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal (↑Γ(X, U) : Type u)
t : Set ι
ht : t.Finite
⊢ X.zeroLocus (↑(⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Set ι) ∅ i), I i) : Set (↑Γ(X, U) : Type u)) =
    (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))) ∪
      (↑U : Set ↥X)ᶜ

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal (↑Γ(X, U) : Type u)
t : Set ι
ht : t.Finite
refine :
  ∀ {i : ι} {t : Set ι} (hit : i ∉ t) (ht : t.Finite)
    (IH :
      X.zeroLocus (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u)) =
        (⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))) ∪ (↑U : Set ↥X)ᶜ),
    X.zeroLocus (↑(⨅ i_1 ∈ insert i t, I i_1) : Set (↑Γ(X, U) : Type u)) =
      (⋃ i_1 ∈ insert i t, X.zeroLocus (↑(I i_1) : Set (↑Γ(X, U) : Type u))) ∪ (↑U : Set ↥X)ᶜ
⊢ X.zeroLocus (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u)) =
    (⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))) ∪ (↑U : Set ↥X)ᶜ

Tactic:
refine ht.induction_on _ (by simp) fun {i t} hit ht IH ↦ ?_
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal (↑Γ(X, U) : Type u)
t_1 : Set ι
ht_1 : t_1.Finite
i : ι
t : Set ι
hit : i ∉ t
ht : t.Finite
IH :
  X.zeroLocus (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u)) =
    (⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))) ∪ (↑U : Set ↥X)ᶜ
simp :
  X.zeroLocus (↑(⨅ (i_1 : ι), ⨅ (_ : i_1 = i ∨ i_1 ∈ t), I i_1) : Set (↑Γ(X, U) : Type u)) =
    X.zeroLocus ((↑(I i) : Set (↑Γ(X, U) : Type u)) ∩ (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u)))
⊢ X.zeroLocus (↑(⨅ i_1 ∈ insert i t, I i_1) : Set (↑Γ(X, U) : Type u)) =
    (⋃ i_1 ∈ insert i t, X.zeroLocus (↑(I i_1) : Set (↑Γ(X, U) : Type u))) ∪ (↑U : Set ↥X)ᶜ

Tactic:
simp only [Set.mem_insert_iff, Set.iUnion_iUnion_eq_or_left, ← IH, ← zeroLocus_inf,
    Submodule.coe_inf, Set.union_assoc]

Premises used: AlgebraicGeometry.Scheme.zeroLocus_inf, Submodule.coe_inf, Set.iUnion_iUnion_eq_or_left, Set.mem_insert_iff, Set.union_assoc
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal (↑Γ(X, U) : Type u)
t_1 : Set ι
ht_1 : t_1.Finite
i : ι
t : Set ι
hit : i ∉ t
ht : t.Finite
IH :
  X.zeroLocus (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u)) =
    (⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))) ∪ (↑U : Set ↥X)ᶜ
h :
  (↑(⨅ (i_1 : ι), ⨅ (_ : i_1 = i ∨ i_1 ∈ t), I i_1) : Set (↑Γ(X, U) : Type u)) =
    (↑(I i) : Set (↑Γ(X, U) : Type u)) ∩ (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u))
⊢ X.zeroLocus (↑(⨅ (i_1 : ι), ⨅ (_ : i_1 = i ∨ i_1 ∈ t), I i_1) : Set (↑Γ(X, U) : Type u)) =
    X.zeroLocus ((↑(I i) : Set (↑Γ(X, U) : Type u)) ∩ (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u)))

Tactic:
congr!
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal (↑Γ(X, U) : Type u)
t_1 : Set ι
ht_1 : t_1.Finite
i : ι
t : Set ι
hit : i ∉ t
ht : t.Finite
IH :
  X.zeroLocus (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u)) =
    (⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))) ∪ (↑U : Set ↥X)ᶜ
⊢ (↑(⨅ (i_1 : ι), ⨅ (_ : i_1 = i ∨ i_1 ∈ t), I i_1) : Set (↑Γ(X, U) : Type u)) =
    (↑(I i) : Set (↑Γ(X, U) : Type u)) ∩ (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal (↑Γ(X, U) : Type u)
t : Set ι
ht : t.Finite
ht' : t.Nonempty
rw : (↑U : Set ↥X)ᶜ ⊆ ⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))
⊢ X.zeroLocus (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u)) = ⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))

Tactic:
rw [zeroLocus_biInf I ht, Set.union_eq_left]

Premises used: Set.union_eq_left, AlgebraicGeometry.Scheme.zeroLocus_biInf
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal (↑Γ(X, U) : Type u)
t : Set ι
ht : t.Finite
ht' : t.Nonempty
obtain : ∀ (i : ι) (hi : i ∈ t), (↑U : Set ↥X)ᶜ ⊆ ⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))
⊢ (↑U : Set ↥X)ᶜ ⊆ ⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))

Tactic:
obtain ⟨i, hi⟩ := ht'
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal (↑Γ(X, U) : Type u)
t : Set ι
ht : t.Finite
i : ι
hi : i ∈ t
⊢ (↑U : Set ↥X)ᶜ ⊆ ⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))

Tactic:
fun x hx ↦ Set.mem_iUnion₂_of_mem hi
    (codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) (I i)) hx)

Premises used: codisjoint_iff_compl_le_left, Set.mem_iUnion₂_of_mem, Set.Subset, SetLike.coe, Iff.mp, AlgebraicGeometry.Scheme.codisjoint_zeroLocus
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal (↑Γ(X, U) : Type u)
t : Set ι
ht : t.Finite
i : ι
hi : i ∈ t
⊢ (↑U : Set ↥X)ᶜ ⊆ ⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))

Tactic:
exact fun x hx ↦ Set.mem_iUnion₂_of_mem hi
    (codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) (I i)) hx)

Premises used: Set.mem_iUnion₂_of_mem
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal (↑Γ(X, U) : Type u)
inst : Finite ι
⊢ X.zeroLocus (↑(⨅ (i : ι), I i) : Set (↑Γ(X, U) : Type u)) =
    (⋃ (i : ι), X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))) ∪ (↑U : Set ↥X)ᶜ

Tactic:
simpa using zeroLocus_biInf I Set.finite_univ

Premises used: AlgebraicGeometry.Scheme.zeroLocus_biInf, Set.finite_univ
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal (↑Γ(X, U) : Type u)
inst : Finite ι
inst_1 : Nonempty ι
⊢ X.zeroLocus (↑(⨅ (i : ι), I i) : Set (↑Γ(X, U) : Type u)) = ⋃ (i : ι), X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))

Tactic:
simpa using zeroLocus_biInf_of_nonempty I Set.finite_univ

Premises used: Set.finite_univ, AlgebraicGeometry.Scheme.zeroLocus_biInf_of_nonempty
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal (↑A : Type u)
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
rw : X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))) = f
⊢ f.liftQuotient I hI ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = f

Tactic:
rw [Scheme.Hom.liftQuotient, Category.assoc, ← Spec.map_comp, ← CommRingCat.ofHom_comp,
    Ideal.Quotient.lift_comp_mk]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.liftQuotient, AlgebraicGeometry.Spec.map_comp, CommRingCat.ofHom_comp, Ideal.Quotient.lift_comp_mk
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal (↑A : Type u)
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
simp : f ≫ Spec.map (ΓSpecIso A).hom ≫ Spec.map (ΓSpecIso A).inv = f
⊢ X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))) = f

Tactic:
simp only [CommRingCat.hom_comp, CommRingCat.ofHom_comp, CommRingCat.ofHom_hom, Spec.map_comp, ←
    Scheme.toSpecΓ_naturality_assoc, ← SpecMap_ΓSpecIso_hom]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, CommRingCat.ofHom_hom, CommRingCat.hom_comp, AlgebraicGeometry.Spec.map_comp, CommRingCat.ofHom_comp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal (↑A : Type u)
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
⊢ f ≫ Spec.map (ΓSpecIso A).hom ≫ Spec.map (ΓSpecIso A).inv = f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
A : CommRingCat
f : X ⟶ Spec A
⊢ Function.Surjective (α := (↑A : Type u)) (β := (↑(specTargetImage f) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (specTargetImageRingHom f)) :
      (a : (↑A : Type u)) → (↑(specTargetImage f) : Type u))

Tactic:
Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
A : CommRingCat
f : X ⟶ Spec A
φ : A ⟶ Γ(X, ⊤) :=
  Quiver.Hom.unop
    ((Equiv.symm (ΓSpec.adjunction.homEquiv X (op A)) :
        (a : X ⟶ Scheme.Spec.obj (op A)) → Scheme.Γ.rightOp.obj X ⟶ op A)
      f)
φ' : specTargetImage f ⟶ Scheme.Γ.obj (op X) := CommRingCat.ofHom (CommRingCat.Hom.hom φ).kerLift
change :
  Function.Injective (α := (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤)) (Y := Γ(X, ⊤))
          (Scheme.Hom.appTop
            ((ΓSpec.adjunction.homEquiv X (op (specTargetImage f)) :
                (a : Scheme.Γ.rightOp.obj X ⟶ op (specTargetImage f)) → X ⟶ Scheme.Spec.obj (op (specTargetImage f)))
              φ'.op))) :
      (a : (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
⊢ Function.Injective (α := (↑Γ(Spec (specTargetImage f), ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop (specTargetImageFactorization f))) :
      (a : (↑Γ(Spec (specTargetImage f), ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))

Tactic:
change Function.Injective <| ((ΓSpec.adjunction.homEquiv X _) φ'.op).appTop

Premises used: Quiver.Hom.op, AlgebraicGeometry.Scheme.Hom.appTop, AlgebraicGeometry.ΓSpec.adjunction, CategoryTheory.Adjunction.homEquiv, Function.Injective, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
A : CommRingCat
f : X ⟶ Spec A
φ : A ⟶ Γ(X, ⊤) :=
  Quiver.Hom.unop
    ((Equiv.symm (ΓSpec.adjunction.homEquiv X (op A)) :
        (a : X ⟶ Scheme.Spec.obj (op A)) → Scheme.Γ.rightOp.obj X ⟶ op A)
      f)
φ' : specTargetImage f ⟶ Scheme.Γ.obj (op X) := CommRingCat.ofHom (CommRingCat.Hom.hom φ).kerLift
rw :
  Function.Injective (α := (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Iso.hom (Scheme.ΓSpecIso (specTargetImage f)) ≫ φ')) :
      (a : (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
⊢ Function.Injective (α := (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤)) (Y := Γ(X, ⊤))
          (Scheme.Hom.appTop
            ((ΓSpec.adjunction.homEquiv X (op (specTargetImage f)) :
                (a : Scheme.Γ.rightOp.obj X ⟶ op (specTargetImage f)) → X ⟶ Scheme.Spec.obj (op (specTargetImage f)))
              φ'.op))) :
      (a : (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))

Tactic:
rw [ΓSpec_adjunction_homEquiv_eq]

Premises used: AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
A : CommRingCat
f : X ⟶ Spec A
φ : A ⟶ Γ(X, ⊤) :=
  Quiver.Hom.unop
    ((Equiv.symm (ΓSpec.adjunction.homEquiv X (op A)) :
        (a : X ⟶ Scheme.Spec.obj (op A)) → Scheme.Γ.rightOp.obj X ⟶ op A)
      f)
φ' : specTargetImage f ⟶ Scheme.Γ.obj (op X) := CommRingCat.ofHom (CommRingCat.Hom.hom φ).kerLift
apply :
  Function.Injective.{u + 1, u + 1} (α := (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) (β :=
    HasQuotient.Quotient (↑A : Type u) (B := Ideal (↑A : Type u)) (RingHom.ker (CommRingCat.Hom.hom φ)))
    (⇑(CommRingCat.Hom.hom' (Iso.hom (Scheme.ΓSpecIso (specTargetImage f)))) :
      (a : (↑Γ(Spec (specTargetImage f), ⊤) : Type u)) → (↑(specTargetImage f) : Type u))
⊢ Function.Injective (α := (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Iso.hom (Scheme.ΓSpecIso (specTargetImage f)) ≫ φ')) :
      (a : (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))

Tactic:
apply (RingHom.kerLift_injective φ.hom).comp

Premises used: CommRingCat.Hom.hom, RingHom.kerLift_injective, Function.Injective.comp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
A : CommRingCat
f : X ⟶ Spec A
φ : A ⟶ Γ(X, ⊤) :=
  Quiver.Hom.unop
    ((Equiv.symm (ΓSpec.adjunction.homEquiv X (op A)) :
        (a : X ⟶ Scheme.Spec.obj (op A)) → Scheme.Γ.rightOp.obj X ⟶ op A)
      f)
φ' : specTargetImage f ⟶ Scheme.Γ.obj (op X) := CommRingCat.ofHom (CommRingCat.Hom.hom φ).kerLift
⊢ Function.Injective.{u + 1, u + 1} (α := (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) (β :=
    HasQuotient.Quotient (↑A : Type u) (B := Ideal (↑A : Type u)) (RingHom.ker (CommRingCat.Hom.hom φ)))
    (⇑(CommRingCat.Hom.hom' (Iso.hom (Scheme.ΓSpecIso (specTargetImage f)))) :
      (a : (↑Γ(Spec (specTargetImage f), ⊤) : Type u)) → (↑(specTargetImage f) : Type u))

Tactic:
((ConcreteCategory.isIso_iff_bijective (Scheme.ΓSpecIso _).hom).mp inferInstance).injective

Premises used: Set.Mem, inferInstance, AlgebraicGeometry.specTargetImage, AlgebraicGeometry.Scheme.ΓSpecIso, Function.Bijective.injective, CategoryTheory.ConcreteCategory.isIso_iff_bijective, Iff.mp, AlgebraicGeometry.specTargetImageIdeal, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
A : CommRingCat
f : X ⟶ Spec A
φ : A ⟶ Γ(X, ⊤) :=
  Quiver.Hom.unop
    ((Equiv.symm (ΓSpec.adjunction.homEquiv X (op A)) :
        (a : X ⟶ Scheme.Spec.obj (op A)) → Scheme.Γ.rightOp.obj X ⟶ op A)
      f)
φ' : specTargetImage f ⟶ Scheme.Γ.obj (op X) := CommRingCat.ofHom (CommRingCat.Hom.hom φ).kerLift
⊢ Function.Injective.{u + 1, u + 1} (α := (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) (β :=
    HasQuotient.Quotient (↑A : Type u) (B := Ideal (↑A : Type u)) (RingHom.ker (CommRingCat.Hom.hom φ)))
    (⇑(CommRingCat.Hom.hom' (Iso.hom (Scheme.ΓSpecIso (specTargetImage f)))) :
      (a : (↑Γ(Spec (specTargetImage f), ⊤) : Type u)) → (↑(specTargetImage f) : Type u))

Tactic:
exact ((ConcreteCategory.isIso_iff_bijective (Scheme.ΓSpecIso _).hom).mp inferInstance).injective

Premises used: inferInstance, AlgebraicGeometry.Scheme.ΓSpecIso, Function.Bijective.injective, CategoryTheory.ConcreteCategory.isIso_iff_bijective, Iff.mp, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
A : CommRingCat
f : X ⟶ Spec A
⊢ specTargetImageFactorization f ≫ Spec.map (specTargetImageRingHom f) = f

Tactic:
f.liftQuotient_comp _ _

Premises used: AlgebraicGeometry.Scheme.Hom.liftQuotient_comp, AlgebraicGeometry.specTargetImage, AlgebraicGeometry.specTargetImageRingHom
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R : CommRingCat
x : PrimeSpectrum (↑R : Type u)
hf :
  ∀ (s : (↑(CommRingCat.of (↑R : Type u)) : Type u)),
    Eq (α := (↑((Spec R).presheaf.stalk x) : Type u))
      ((CommRingCat.Hom.hom
              (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.AtPrime x.asIdeal)) ≫ (stalkIso R x).inv) :
            (a : (↑(CommRingCat.of (↑R : Type u)) : Type u)) → (↑((Spec R).presheaf.stalk x) : Type u))
          s :
        (↑((Spec R).presheaf.stalk x) : Type u))
      ((CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial) :
            (a : (↑(CommRingCat.of (↑R : Type u)) : Type u)) → (↑((Spec R).presheaf.stalk x) : Type u))
          s :
        (↑((Spec R).presheaf.stalk x) : Type u))
⊢ CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.AtPrime x.asIdeal)) ≫ (stalkIso R x).inv =
    (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial

Tactic:
ext s : 2
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R : CommRingCat
x : PrimeSpectrum (↑R : Type u)
s : (↑(CommRingCat.of (↑R : Type u)) : Type u)
⊢ Eq (α := (↑((Spec R).presheaf.stalk x) : Type u))
    ((CommRingCat.Hom.hom
            (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.AtPrime x.asIdeal)) ≫ (stalkIso R x).inv) :
          (a : (↑(CommRingCat.of (↑R : Type u)) : Type u)) → (↑((Spec R).presheaf.stalk x) : Type u))
        s :
      (↑((Spec R).presheaf.stalk x) : Type u))
    ((CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial) :
          (a : (↑(CommRingCat.of (↑R : Type u)) : Type u)) → (↑((Spec R).presheaf.stalk x) : Type u))
        s :
      (↑((Spec R).presheaf.stalk x) : Type u))

Tactic:
(IsLocalization.algEquiv _ ((structureSheaf R).presheaf.stalk _) _).symm.commutes s

Premises used: CommRingCat.carrier, AlgEquiv.symm, AlgebraicGeometry.Spec.topObj, Set.Mem, setOf, AlgEquiv.commutes, TopCat.Presheaf.stalk, IsLocalization.algEquiv, AlgebraicGeometry.Spec.structureSheaf, AlgebraicGeometry.PrimeSpectrum.Top, AlgebraicGeometry.structurePresheafInCommRingCat, TopCat.Sheaf.presheaf
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R : CommRingCat
x : PrimeSpectrum (↑R : Type u)
s : (↑(CommRingCat.of (↑R : Type u)) : Type u)
⊢ Eq (α := (↑((Spec R).presheaf.stalk x) : Type u))
    ((CommRingCat.Hom.hom
            (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.AtPrime x.asIdeal)) ≫ (stalkIso R x).inv) :
          (a : (↑(CommRingCat.of (↑R : Type u)) : Type u)) → (↑((Spec R).presheaf.stalk x) : Type u))
        s :
      (↑((Spec R).presheaf.stalk x) : Type u))
    ((CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial) :
          (a : (↑(CommRingCat.of (↑R : Type u)) : Type u)) → (↑((Spec R).presheaf.stalk x) : Type u))
        s :
      (↑((Spec R).presheaf.stalk x) : Type u))

Tactic:
exact (IsLocalization.algEquiv _ ((structureSheaf R).presheaf.stalk _) _).symm.commutes s

Premises used: CommRingCat.carrier, AlgEquiv.symm, AlgEquiv.commutes, TopCat.Presheaf.stalk, IsLocalization.algEquiv, AlgebraicGeometry.Spec.structureSheaf, TopCat.Sheaf.presheaf
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R : CommRingCat
x : PrimeSpectrum (↑R : Type u)
⊢ (Spec R).presheaf.germ ⊤ x trivial ≫ (stalkIso R x).hom =
    (Scheme.ΓSpecIso R).hom ≫ CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.AtPrime x.asIdeal))

Tactic:
simp [← Iso.inv_comp_eq, ← Spec.algebraMap_stalkIso_inv_assoc]

Premises used: CategoryTheory.Iso.inv_comp_eq, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc