awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : (↑Γ(X, U) : Type u)
e :
  f ⁻¹ᵁ
      Y.basicOpen (U := f ''ᵁ U)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
          r) =
    X.basicOpen (U := f ⁻¹ᵁ f ''ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, f ''ᵁ U)) (Hom.app f (f ''ᵁ U)) :
          (a : (↑Γ(Y, f ''ᵁ U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ f ''ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
            r :
          (↑Γ(Y, f ''ᵁ U) : Type u)))
rw :
  ∀
    (e :
      f ⁻¹ᵁ
          Y.basicOpen (U := f ''ᵁ U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
                (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
              r) =
        X.basicOpen r),
    f ''ᵁ X.basicOpen r =
      Y.basicOpen (U := f ''ᵁ U)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
          r)
rw₁ :
  ∀
    (e :
      f ⁻¹ᵁ
          Y.basicOpen (U := f ''ᵁ U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
                (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
              r) =
        f ⁻¹ᵁ f ''ᵁ U ⊓ X.basicOpen r),
    X.basicOpen r ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ f ''ᵁ X.basicOpen r =
    Y.basicOpen (U := f ''ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
        r)

Tactic:
rw [Scheme.Hom.appIso_inv_app_apply, Scheme.basicOpen_res, inf_eq_right.mpr _] at e

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.basicOpen_res, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply, inf_eq_right
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : (↑Γ(X, U) : Type u)
e :
  f ⁻¹ᵁ
      Y.basicOpen (U := f ''ᵁ U)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
          r) =
    X.basicOpen r
rw :
  Y.basicOpen (U := f ''ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
        r) ≤
    Hom.opensRange f
⊢ f ''ᵁ X.basicOpen r =
    Y.basicOpen (U := f ''ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
        r)

Tactic:
rw [← e, f.image_preimage_eq_opensRange_inf, inf_eq_right]

Premises used: AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, inf_eq_right
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : (↑Γ(X, U) : Type u)
e :
  f ⁻¹ᵁ
      Y.basicOpen (U := f ''ᵁ U)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
          r) =
    X.basicOpen r
⊢ Y.basicOpen (U := f ''ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
        r) ≤
    Hom.opensRange f

Tactic:
Set.Subset.trans (Scheme.basicOpen_le _ _) (Set.image_subset_range _ _)

Premises used: Set.Subset.trans, AlgebraicGeometry.Scheme.basicOpen_le, Set.image_subset_range, Set.Subset
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : (↑Γ(X, U) : Type u)
e :
  f ⁻¹ᵁ
      Y.basicOpen (U := f ''ᵁ U)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
          r) =
    X.basicOpen r
⊢ Y.basicOpen (U := f ''ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
        r) ≤
    Hom.opensRange f

Tactic:
refine Set.Subset.trans (Scheme.basicOpen_le _ _) (Set.image_subset_range _ _)

Premises used: Set.Subset.trans, AlgebraicGeometry.Scheme.basicOpen_le
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : (↑Γ(X, U) : Type u)
e :
  f ⁻¹ᵁ
      Y.basicOpen (U := f ''ᵁ U)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
          r) =
    f ⁻¹ᵁ f ''ᵁ U ⊓ X.basicOpen r
⊢ X.basicOpen r ≤ f ⁻¹ᵁ f ''ᵁ U

Tactic:
(X.basicOpen_le r).trans (f.preimage_image_eq _).ge

Premises used: Eq.ge, AlgebraicGeometry.Scheme.Hom.preimage_image_eq, AlgebraicGeometry.Scheme.basicOpen_le, LE.le.trans
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : (↑Γ(X, U) : Type u)
e :
  f ⁻¹ᵁ
      Y.basicOpen (U := f ''ᵁ U)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
          r) =
    f ⁻¹ᵁ f ''ᵁ U ⊓ X.basicOpen r
⊢ X.basicOpen r ≤ f ⁻¹ᵁ f ''ᵁ U

Tactic:
exact (X.basicOpen_le r).trans (f.preimage_image_eq _).ge

Premises used: Eq.ge, AlgebraicGeometry.Scheme.Hom.preimage_image_eq, AlgebraicGeometry.Scheme.basicOpen_le, LE.le.trans
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
h :
  ∀ (x : ↥Y),
    Membership.mem (γ := Set ↥Y) (⇑f '' X.zeroLocus s) x ↔
      x ∈
        Y.zeroLocus (U := f ''ᵁ U)
            ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) :
                (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
              s) ∩
          Set.range (ι := ↥X) ⇑f
⊢ ⇑f '' X.zeroLocus s =
    Y.zeroLocus (U := f ''ᵁ U)
        ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) : (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
          s) ∩
      Set.range (ι := ↥X) ⇑f

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥Y
pos :
  ∀ (hx : Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥X) ⇑f) x),
    Membership.mem (γ := Set ↥Y) (⇑f '' X.zeroLocus s) x ↔
      x ∈
        Y.zeroLocus (U := f ''ᵁ U)
            ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) :
                (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
              s) ∩
          Set.range (ι := ↥X) ⇑f
neg :
  ∀ (hx : x ∉ Set.range (ι := ↥X) ⇑f),
    Membership.mem (γ := Set ↥Y) (⇑f '' X.zeroLocus s) x ↔
      x ∈
        Y.zeroLocus (U := f ''ᵁ U)
            ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) :
                (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
              s) ∩
          Set.range (ι := ↥X) ⇑f
⊢ Membership.mem (γ := Set ↥Y) (⇑f '' X.zeroLocus s) x ↔
    x ∈
      Y.zeroLocus (U := f ''ᵁ U)
          ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
            s) ∩
        Set.range (ι := ↥X) ⇑f

Tactic:
by_cases hx : x ∈ Set.range f

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, Set.range, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥Y
hx : Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥X) ⇑f) x
pos :
  ∀ (x : ↥X),
    Membership.mem (α := ↥Y) (γ := Set ↥Y) (⇑f '' X.zeroLocus s) (f x : ↥Y) ↔
      Membership.mem (α := ↥Y)
        (Y.zeroLocus (U := f ''ᵁ U)
            ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) :
                (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
              s) ∩
          Set.range (ι := ↥X) ⇑f)
        (f x : ↥Y)
⊢ Membership.mem (γ := Set ↥Y) (⇑f '' X.zeroLocus s) x ↔
    x ∈
      Y.zeroLocus (U := f ''ᵁ U)
          ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
            s) ∩
        Set.range (ι := ↥X) ⇑f

Tactic:
obtain ⟨x, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥Y
hx : x ∉ Set.range (ι := ↥X) ⇑f
neg : x ∉ (fun (a : ↥X) ↦ f a) '' X.zeroLocus s
⊢ Membership.mem (γ := Set ↥Y) (⇑f '' X.zeroLocus s) x ↔
    x ∈
      Y.zeroLocus (U := f ''ᵁ U)
          ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
            s) ∩
        Set.range (ι := ↥X) ⇑f

Tactic:
simp only [Set.mem_inter_iff, hx, and_false, iff_false]

Premises used: iff_false, Set.mem_inter_iff, and_false
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥Y
hx : x ∉ Set.range (ι := ↥X) ⇑f
⊢ x ∉ (fun (a : ↥X) ↦ f a) '' X.zeroLocus s

Tactic:
fun H ↦ hx (Set.image_subset_range _ _ H)

Premises used: CategoryTheory.ConcreteCategory.hom, Set.image_subset_range, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.zeroLocus, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, Not
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥Y
hx : x ∉ Set.range (ι := ↥X) ⇑f
⊢ x ∉ (fun (a : ↥X) ↦ f a) '' X.zeroLocus s

Tactic:
exact fun H ↦ hx (Set.image_subset_range _ _ H)

Premises used: CategoryTheory.ConcreteCategory.hom, Set.image_subset_range, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst_1 : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
rw : Eq (α := ↥Z) ((snd ≫ g) p : ↥Z) (g (snd p : ↥Y) : ↥Z)
⊢ Eq (α := ↥Z) (f x : ↥Z) (g (snd p : ↥Y) : ↥Z)

Tactic:
rw [← hx, ← Scheme.Hom.comp_apply, h.w]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst_1 : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
⊢ Eq (α := ↥Z) ((snd ≫ g) p : ↥Z) (g (snd p : ↥Y) : ↥Z)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst_1 : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
rw rw₁ : x = x
⊢ x = fst p

Tactic:
rw [hx]
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst_1 : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
subst :
  Eq (α := Z.presheaf.stalk (f (fst p : ↥X)) ⟶ P.presheaf.stalk p)
    (Iso.hom (Z.presheaf.stalkCongr ⋯ ≪≫ asIso (Hom.stalkMap g (snd p))) ≫ Hom.stalkMap snd p)
    (Hom.stalkMap f (fst p) ≫ Iso.hom (X.presheaf.stalkCongr ⋯ ≪≫ asIso (Hom.stalkMap fst p)))
⊢ (Z.presheaf.stalkCongr ⋯ ≪≫ asIso (Hom.stalkMap g (snd p))).hom ≫ Hom.stalkMap snd p =
    Hom.stalkMap f x ≫ (X.presheaf.stalkCongr ⋯ ≪≫ asIso (Hom.stalkMap fst p)).hom

Tactic:
subst hx
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst_1 : IsOpenImmersion g
p : ↥P
this : IsOpenImmersion fst
⊢ Eq (α := Z.presheaf.stalk (f (fst p : ↥X)) ⟶ P.presheaf.stalk p)
    (Iso.hom (Z.presheaf.stalkCongr ⋯ ≪≫ asIso (Hom.stalkMap g (snd p))) ≫ Hom.stalkMap snd p)
    (Hom.stalkMap f (fst p) ≫ Iso.hom (X.presheaf.stalkCongr ⋯ ≪≫ asIso (Hom.stalkMap fst p)))

Tactic:
simp [← Scheme.Hom.stalkMap_comp, ← Scheme.Hom.stalkMap_comp,
        Scheme.Hom.stalkMap_congr_hom _ _ h.w]

Premises used: AlgebraicGeometry.Scheme.Hom.stalkMap_comp, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom
-- Module: Mathlib.AlgebraicGeometry.Over
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X ⟶ Y
⊢ IsOver f S ↔ f ≫ Y ↘ S = X ↘ S

Tactic:
⟨fun H ↦ H.1, fun h ↦ ⟨h⟩⟩

Premises used: CategoryTheory.HomIsOver.mk, Iff.intro, CategoryTheory.HomIsOver.comp_over
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u_2
R : ι → Type u_1
inst : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
hs' :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := Ideal (R i))
      (Ideal.span ((⇑(Pi.evalRingHom (fun (x : ι) ↦ R x) i) : (a : (i : ι) → R i) → R i) '' s)) ⊤
simp :
  ∀
    (hs' :
      ∀ (i : ι),
        ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ R i),
          Eq (α := R i)
            (c.sum fun (i_1 : { x : (i : ι) → R i // x ∈ s }) (a : R i) ↦
              a *
                ((⇑(Pi.evalRingHom (fun (x : ι) ↦ R x) i) : (a : (i : ι) → R i) → R i) ∘
                    Subtype.val (p := fun (x : (i : ι) → R i) ↦ x ∈ s))
                  i_1)
            1),
    ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i),
      Eq (α := (i : ι) → R i)
        (c.sum fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i)) 1
⊢ Eq (α := Ideal ((i : ι) → R i)) (Ideal.span s) ⊤

Tactic:
simp only [Ideal.eq_top_iff_one, ← Subtype.range_val (s := s), ← Set.range_comp,
    Finsupp.mem_ideal_span_range_iff_exists_finsupp] at hs' ⊢

Premises used: Set.range_comp, Subtype.range_val, Ideal.eq_top_iff_one, Finsupp.mem_ideal_span_range_iff_exists_finsupp
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u_2
R : ι → Type u_1
inst : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
hs' :
  ∀ (i : ι),
    ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ R i),
      Eq (α := R i)
        (c.sum fun (i_1 : { x : (i : ι) → R i // x ∈ s }) (a : R i) ↦
          a *
            ((⇑(Pi.evalRingHom (fun (x : ι) ↦ R x) i) : (a : (i : ι) → R i) → R i) ∘
                Subtype.val (p := fun (x : (i : ι) → R i) ↦ x ∈ s))
              i_1)
        1
choose :
  ∀ (f : (i : ι) → { x : (i : ι) → R i // x ∈ s } →₀ R i)
    (hf :
      ∀ (i : ι),
        Eq (α := R i)
          ((f i).sum fun (i_1 : { x : (i : ι) → R i // x ∈ s }) (a : R i) ↦
            a *
              ((⇑(Pi.evalRingHom (fun (x : ι) ↦ R x) i) : (a : (i : ι) → R i) → R i) ∘
                  Subtype.val (p := fun (x : (i : ι) → R i) ↦ x ∈ s))
                i_1)
          1),
    ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i),
      Eq (α := (i : ι) → R i)
        (c.sum fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i)) 1
⊢ ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i),
    Eq (α := (i : ι) → R i)
      (c.sum fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i)) 1

Tactic:
choose f hf using hs'
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u_2
R : ι → Type u_1
inst : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x : (i : ι) → R i // x ∈ s } →₀ R i
hf :
  ∀ (i : ι),
    Eq (α := R i)
      ((f i).sum fun (i_1 : { x : (i : ι) → R i // x ∈ s }) (a : R i) ↦
        a *
          ((⇑(Pi.evalRingHom (fun (x : ι) ↦ R x) i) : (a : (i : ι) → R i) → R i) ∘
              Subtype.val (p := fun (x : (i : ι) → R i) ↦ x ∈ s))
            i_1)
      1
have :
  ∀ (this : Fintype (↑s : Type (max u_1 u_2))),
    ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i),
      Eq (α := (i : ι) → R i)
        (c.sum fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i)) 1
⊢ ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i),
    Eq (α := (i : ι) → R i)
      (c.sum fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i)) 1

Tactic:
have : Fintype s := hs.fintype
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u_2
R : ι → Type u_1
inst : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x : (i : ι) → R i // x ∈ s } →₀ R i
hf :
  ∀ (i : ι),
    Eq (α := R i)
      ((f i).sum fun (i_1 : { x : (i : ι) → R i // x ∈ s }) (a : R i) ↦
        a *
          ((⇑(Pi.evalRingHom (fun (x : ι) ↦ R x) i) : (a : (i : ι) → R i) → R i) ∘
              Subtype.val (p := fun (x : (i : ι) → R i) ↦ x ∈ s))
            i_1)
      1
this : Fintype (↑s : Type (max u_1 u_2))
⊢ ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i),
    Eq (α := (i : ι) → R i)
      (c.sum fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i)) 1

Tactic:
⟨Finsupp.equivFunOnFinite.symm fun i x ↦ f x i, ?_⟩

Premises used: Finsupp.equivFunOnFinite, Exists.intro, Equiv.symm, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u_2
R : ι → Type u_1
inst : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x : (i : ι) → R i // x ∈ s } →₀ R i
hf :
  ∀ (i : ι),
    Eq (α := R i)
      ((f i).sum fun (i_1 : { x : (i : ι) → R i // x ∈ s }) (a : R i) ↦
        a *
          ((⇑(Pi.evalRingHom (fun (x : ι) ↦ R x) i) : (a : (i : ι) → R i) → R i) ∘
              Subtype.val (p := fun (x : (i : ι) → R i) ↦ x ∈ s))
            i_1)
      1
this : Fintype (↑s : Type (max u_1 u_2))
refine :
  Eq (α := (i : ι) → R i)
    (Finsupp.sum
      ((Equiv.symm Finsupp.equivFunOnFinite :
          (a : { x : (i : ι) → R i // x ∈ s } → (i : ι) → R i) → { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i)
        fun (i : { x : (i : ι) → R i // x ∈ s }) (x : ι) ↦ (f x : (a : { x : (i : ι) → R i // x ∈ s }) → R x) i)
      fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i))
    1
⊢ ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i),
    Eq (α := (i : ι) → R i)
      (c.sum fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i)) 1

Tactic:
refine ⟨Finsupp.equivFunOnFinite.symm fun i x ↦ f x i, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u_2
R : ι → Type u_1
inst : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x : (i : ι) → R i // x ∈ s } →₀ R i
hf :
  ∀ (i : ι),
    Eq (α := R i)
      ((f i).sum fun (i_1 : { x : (i : ι) → R i // x ∈ s }) (a : R i) ↦
        a *
          ((⇑(Pi.evalRingHom (fun (x : ι) ↦ R x) i) : (a : (i : ι) → R i) → R i) ∘
              Subtype.val (p := fun (x : (i : ι) → R i) ↦ x ∈ s))
            i_1)
      1
this : Fintype (↑s : Type (max u_1 u_2))
h :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := R i)
      (Finsupp.sum
        ((Equiv.symm Finsupp.equivFunOnFinite :
            (a : { x : (i : ι) → R i // x ∈ s } → (i : ι) → R i) → { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i)
          fun (i : { x : (i : ι) → R i // x ∈ s }) (x : ι) ↦ (f x : (a : { x : (i : ι) → R i // x ∈ s }) → R x) i)
        (fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i)) i)
      (1 i)
⊢ Eq (α := (i : ι) → R i)
    (Finsupp.sum
      ((Equiv.symm Finsupp.equivFunOnFinite :
          (a : { x : (i : ι) → R i // x ∈ s } → (i : ι) → R i) → { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i)
        fun (i : { x : (i : ι) → R i // x ∈ s }) (x : ι) ↦ (f x : (a : { x : (i : ι) → R i // x ∈ s }) → R x) i)
      fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i))
    1

Tactic:
ext i
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u_2
R : ι → Type u_1
inst : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x : (i : ι) → R i // x ∈ s } →₀ R i
hf :
  ∀ (i : ι),
    Eq (α := R i)
      ((f i).sum fun (i_1 : { x : (i : ι) → R i // x ∈ s }) (a : R i) ↦
        a *
          ((⇑(Pi.evalRingHom (fun (x : ι) ↦ R x) i) : (a : (i : ι) → R i) → R i) ∘
              Subtype.val (p := fun (x : (i : ι) → R i) ↦ x ∈ s))
            i_1)
      1
this : Fintype (↑s : Type (max u_1 u_2))
i : ι
⊢ Eq.{u_1 + 1} (α := R i)
    (Finsupp.sum
      ((Equiv.symm Finsupp.equivFunOnFinite :
          (a : { x : (i : ι) → R i // x ∈ s } → (i : ι) → R i) → { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i)
        fun (i : { x : (i : ι) → R i // x ∈ s }) (x : ι) ↦ (f x : (a : { x : (i : ι) → R i // x ∈ s }) → R x) i)
      (fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i)) i)
    (1 i)

Tactic:
simpa [Finsupp.sum_fintype] using hf i

Premises used: Finsupp.sum_fintype
-- Module: Mathlib.AlgebraicGeometry.PointsPi
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
obtain : ∀ (s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)) (hs : U.carrierᶜ = zeroLocus s), U = ⊤
⊢ U = ⊤

Tactic:
obtain ⟨s, hs⟩ := (PrimeSpectrum.isOpen_iff _).mp U.2

Premises used: PrimeSpectrum.isOpen_iff, Iff.mp, TopologicalSpace.Opens.is_open'