-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
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 :
  ∀ (x : ↥(↑V : X.Opens)),
    ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
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
have₂ :
  ∀ (x : ↥(↑V : X.Opens)),
    ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
have₃ 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
have₅ :
  ∀ (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
have₆ :
  ∀ (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))),
    Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (Set.range f)) ⊤
have₇ :
  ∀ (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))),
    (↑V : X.Opens) ≤ ⨆ (f_1 : (↑(Set.range f) : Type u_1)), X.basicOpen (↑f_1 : (↑Γ(X, (↑V : X.Opens)) : Type u_1))
have₈ :
  ∀ (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)),
    Membership.mem (γ := Opens ↥X)
      (⨆ (f_1 : (↑(Set.range f) : Type u_1)), X.basicOpen (↑f_1 : (↑Γ(X, (↑V : X.Opens)) : Type u_1))) x
⊢ P V
have have₉ : ∀ (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: classical
  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
  choose f hf₁ hf₂ using this
  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
  rw [← V.prop.self_le_iSup_basicOpen_iff]
  intro x hx
  rw [iSup_range', Opens.mem_iSup]
  exact ⟨_, hf₁ ⟨x, hx⟩⟩