awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
x : ↥(↑V : X.Opens)
i : ι
hi : (↑x : ↥X) ∈ (↑(U i) : X.Opens)
f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)
g : (↑Γ(X, (↑(U i) : X.Opens)) : Type u_1)
e : X.basicOpen f = X.basicOpen g
hf : (↑x : ↥X) ∈ X.basicOpen f
⊢ ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)

Tactic:
⟨f, hf, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
x : ↥(↑V : X.Opens)
i : ι
hi : (↑x : ↥X) ∈ (↑(U i) : X.Opens)
f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)
g : (↑Γ(X, (↑(U i) : X.Opens)) : Type u_1)
e : X.basicOpen f = X.basicOpen g
hf : (↑x : ↥X) ∈ X.basicOpen f
refine : P (X.affineBasicOpen f)
⊢ ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)

Tactic:
refine ⟨f, hf, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
x : ↥(↑V : X.Opens)
i : ι
hi : (↑x : ↥X) ∈ (↑(U i) : X.Opens)
f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)
g : (↑Γ(X, (↑(U i) : X.Opens)) : Type u_1)
e : X.basicOpen f = X.basicOpen g
hf : (↑x : ↥X) ∈ X.basicOpen f
⊢ P (X.affineBasicOpen g)

Tactic:
basicOpen _ g (hU i)
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
x : ↥(↑V : X.Opens)
i : ι
hi : (↑x : ↥X) ∈ (↑(U i) : X.Opens)
f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)
g : (↑Γ(X, (↑(U i) : X.Opens)) : Type u_1)
e : X.basicOpen f = X.basicOpen g
hf : (↑x : ↥X) ∈ X.basicOpen f
h : X.affineBasicOpen f = X.affineBasicOpen g
⊢ P (X.affineBasicOpen f)

Tactic:
convert! basicOpen _ g (hU i) using 1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
x : ↥(↑V : X.Opens)
i : ι
hi : (↑x : ↥X) ∈ (↑(U i) : X.Opens)
f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)
g : (↑Γ(X, (↑(U i) : X.Opens)) : Type u_1)
e : X.basicOpen f = X.basicOpen g
hf : (↑x : ↥X) ∈ X.basicOpen f
h : (↑(X.affineBasicOpen f) : X.Opens) = (↑(X.affineBasicOpen g) : X.Opens)
⊢ X.affineBasicOpen f = X.affineBasicOpen g

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
x : ↥(↑V : X.Opens)
i : ι
hi : (↑x : ↥X) ∈ (↑(U i) : X.Opens)
f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)
g : (↑Γ(X, (↑(U i) : X.Opens)) : Type u_1)
e : X.basicOpen f = X.basicOpen g
hf : (↑x : ↥X) ∈ X.basicOpen f
⊢ (↑(X.affineBasicOpen f) : X.Opens) = (↑(X.affineBasicOpen g) : X.Opens)

Tactic:
e

Premises used: AlgebraicGeometry.RingedSpace.basicOpen, AlgebraicGeometry.Scheme.basicOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
x : ↥(↑V : X.Opens)
i : ι
hi : (↑x : ↥X) ∈ (↑(U i) : X.Opens)
f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)
g : (↑Γ(X, (↑(U i) : X.Opens)) : Type u_1)
e : X.basicOpen f = X.basicOpen g
hf : (↑x : ↥X) ∈ X.basicOpen f
⊢ (↑(X.affineBasicOpen f) : X.Opens) = (↑(X.affineBasicOpen g) : X.Opens)

Tactic:
exact e
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
have :
  ∀
    (this :
      ∀ (x : ↥(↑V : X.Opens)),
        ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)),
    P V
⊢ P V

Tactic:
have : ∀ (x : V.1), ∃ f : Γ(X, V), ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f) := by
    intro x
    obtain ⟨i, hi⟩ := Opens.mem_iSup.mp (iSup_U.ge (Set.mem_univ x))
    obtain ⟨f, g, e, hf⟩ := exists_basicOpen_le_affine_inter V.prop (U i).prop x ⟨x.prop, hi⟩
    refine ⟨f, hf, ?_⟩
    convert! basicOpen _ g (hU i) using 1
    ext1
    exact e
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
this :
  ∀ (x : ↥(↑V : X.Opens)),
    ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
choose :
  ∀ (f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1))
    (hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x))
    (hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))), P V
⊢ P V

Tactic:
choose f hf₁ hf₂ using this
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))
this : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (Set.range f)) ⊤
obtain :
  ∀ (t : Finset (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (ht₁ : (↑t : Set (↑Γ(X, (↑V : X.Opens)) : Type u_1)) ⊆ Set.range f)
    (ht₂ :
      Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (↑t : Set (↑Γ(X, (↑V : X.Opens)) : Type u_1))) ⊤),
    P V
⊢ P V

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := (Ideal.span_eq_top_iff_finite _).mp this

Premises used: Ideal.span_eq_top_iff_finite, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))
this : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (Set.range f)) ⊤
t : Finset (↑Γ(X, (↑V : X.Opens)) : Type u_1)
ht₁ : (↑t : Set (↑Γ(X, (↑V : X.Opens)) : Type u_1)) ⊆ Set.range f
ht₂ : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (↑t : Set (↑Γ(X, (↑V : X.Opens)) : Type u_1))) ⊤
apply : ∀ (f : ↥t), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)))
⊢ P V

Tactic:
apply openCover V t ht₂
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))
this : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (Set.range f)) ⊤
t : Finset (↑Γ(X, (↑V : X.Opens)) : Type u_1)
ht₁ : (↑t : Set (↑Γ(X, (↑V : X.Opens)) : Type u_1)) ⊆ Set.range f
ht₂ : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (↑t : Set (↑Γ(X, (↑V : X.Opens)) : Type u_1))) ⊤
i : (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hi : i ∈ t
obtain :
  ∀ (x : ↥(↑V : X.Opens)) (hi : f x ∈ t),
    P
      (X.affineBasicOpen
        (↑(Subtype.mk (p := fun (x : (↑Γ(X, (↑V : X.Opens)) : Type u_1)) ↦ x ∈ t) (f x) hi) :
          (↑Γ(X, (↑V : X.Opens)) : Type u_1)))
⊢ P
    (X.affineBasicOpen
      (↑(Subtype.mk (p := fun (x : (↑Γ(X, (↑V : X.Opens)) : Type u_1)) ↦ x ∈ t) i hi) :
        (↑Γ(X, (↑V : X.Opens)) : Type u_1)))

Tactic:
obtain ⟨x, rfl⟩ := ht₁ hi

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))
this : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (Set.range f)) ⊤
t : Finset (↑Γ(X, (↑V : X.Opens)) : Type u_1)
ht₁ : (↑t : Set (↑Γ(X, (↑V : X.Opens)) : Type u_1)) ⊆ Set.range f
ht₂ : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (↑t : Set (↑Γ(X, (↑V : X.Opens)) : Type u_1))) ⊤
x : ↥(↑V : X.Opens)
hi : f x ∈ t
⊢ P
    (X.affineBasicOpen
      (↑(Subtype.mk (p := fun (x : (↑Γ(X, (↑V : X.Opens)) : Type u_1)) ↦ x ∈ t) (f x) hi) :
        (↑Γ(X, (↑V : X.Opens)) : Type u_1)))

Tactic:
hf₂ x
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))
this : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (Set.range f)) ⊤
t : Finset (↑Γ(X, (↑V : X.Opens)) : Type u_1)
ht₁ : (↑t : Set (↑Γ(X, (↑V : X.Opens)) : Type u_1)) ⊆ Set.range f
ht₂ : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (↑t : Set (↑Γ(X, (↑V : X.Opens)) : Type u_1))) ⊤
x : ↥(↑V : X.Opens)
hi : f x ∈ t
⊢ P
    (X.affineBasicOpen
      (↑(Subtype.mk (p := fun (x : (↑Γ(X, (↑V : X.Opens)) : Type u_1)) ↦ x ∈ t) (f x) hi) :
        (↑Γ(X, (↑V : X.Opens)) : Type u_1)))

Tactic:
exact hf₂ x
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))
suffices : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (Set.range f)) ⊤
⊢ P V

Tactic:
suffices Ideal.span (Set.range f) = ⊤ by
    obtain ⟨t, ht₁, ht₂⟩ := (Ideal.span_eq_top_iff_finite _).mp this
    apply openCover V t ht₂
    rintro ⟨i, hi⟩
    obtain ⟨x, rfl⟩ := ht₁ hi
    exact hf₂ x
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))
rw : (↑V : X.Opens) ≤ ⨆ (f_1 : (↑(Set.range f) : Type u_1)), X.basicOpen (↑f_1 : (↑Γ(X, (↑V : X.Opens)) : Type u_1))
⊢ Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (Set.range f)) ⊤

Tactic:
rw [← V.prop.self_le_iSup_basicOpen_iff]

Premises used: AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, Subtype.prop
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))
x : ↥X
hx : x ∈ (↑V : X.Opens)
rw : ∃ (i : ↥(↑V : X.Opens)), x ∈ X.basicOpen (f i)
⊢ Membership.mem (γ := Opens ↥X)
    (⨆ (f_1 : (↑(Set.range f) : Type u_1)), X.basicOpen (↑f_1 : (↑Γ(X, (↑V : X.Opens)) : Type u_1))) x

Tactic:
rw [iSup_range', Opens.mem_iSup]

Premises used: iSup_range', TopologicalSpace.Opens.mem_iSup
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))
x : ↥X
hx : x ∈ (↑V : X.Opens)
⊢ ∃ (i : ↥(↑V : X.Opens)), x ∈ X.basicOpen (f i)

Tactic:
⟨_, hf₁ ⟨x, hx⟩⟩

Premises used: Subtype.mk, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))
x : ↥X
hx : x ∈ (↑V : X.Opens)
⊢ ∃ (i : ↥(↑V : X.Opens)), x ∈ X.basicOpen (f i)

Tactic:
exact ⟨_, hf₁ ⟨x, hx⟩⟩
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
⊢ Mono φ

Tactic:
have : Mono φ := ConcreteCategory.mono_of_injective _ hφ
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ Subset (α := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)

Tactic:
simpa [Set.range_subset_iff] using fun x hx ↦ hUf.ge hx

Premises used: Eq.ge, Set.range_subset_iff