awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
⊢ Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
        (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (I.ideal U ⊓ J.ideal U))
      (IsLocalization.mk' (↑Γ(X, X.basicOpen f) : Type u) x s) ↔
    Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
          (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (I.ideal U) ⊓
        Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
          (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (J.ideal U))
      (IsLocalization.mk' (↑Γ(X, X.basicOpen f) : Type u) x s)
have h : (∃ (a : ℕ), f ^ a * x ∈ I.ideal U ∧ f ^ a * x ∈ J.ideal U) ↔
  (∃ (a : ℕ), f ^ a * x ∈ I.ideal U) ∧ ∃ (a : ℕ), f ^ a * x ∈ J.ideal U
Tactic: simp only [IsLocalization.mk'_mem_map_algebraMap_iff, Submonoid.mem_powers_iff, Ideal.mem_inf,
        exists_exists_eq_and]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
⊢ (∃ (a : ℕ), f ^ a * x ∈ I.ideal U ∧ f ^ a * x ∈ J.ideal U) ↔
    (∃ (a : ℕ), f ^ a * x ∈ I.ideal U) ∧ ∃ (a : ℕ), f ^ a * x ∈ J.ideal U
have h : ((∃ (a : ℕ), f ^ a * x ∈ I.ideal U) ∧ ∃ (a : ℕ), f ^ a * x ∈ J.ideal U) →
  ∃ (a : ℕ), f ^ a * x ∈ I.ideal U ∧ f ^ a * x ∈ J.ideal U
Tactic: refine ⟨fun ⟨n, h₁, h₂⟩ ↦ ⟨⟨n, h₁⟩, ⟨n, h₂⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ ∃ (a : ℕ), f ^ a * x ∈ I.ideal U ∧ f ^ a * x ∈ J.ideal U
have h : f ^ (n₁ + n₂) * x ∈ I.ideal U
Tactic: refine ⟨n₁ + n₂, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
h : f ^ (n₁ + n₂) * x ∈ I.ideal U
⊢ ∃ (a : ℕ), f ^ a * x ∈ I.ideal U ∧ f ^ a * x ∈ J.ideal U
have h₃ : f ^ (n₁ + n₂) * x ∈ J.ideal U
Tactic: refine ⟨n₁ + n₂, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ (n₁ + n₂) * x ∈ I.ideal U
have h : f ^ n₂ * (f ^ n₁ * x) ∈ I.ideal U
Tactic: rw [add_comm, pow_add, mul_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ (n₁ + n₂) * x ∈ J.ideal U
have h : f ^ n₁ * (f ^ n₂ * x) ∈ J.ideal U
Tactic: rw [pow_add, mul_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
⊢ (iSup I).ideal = ⨆ (i : ι), (I i).ideal
have rw : (sSup (Set.range I)).ideal = ⨆ (i : ι), (I i).ideal
Tactic: rw [← sSup_range, ← sSup_range, ideal_sSup, ← Set.range_comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
rw : (sSup (Set.range I)).ideal = ⨆ (i : ι), (I i).ideal
⊢ (iSup I).ideal = ⨆ (i : ι), (I i).ideal
have rw₁ : (sSup (Set.range I)).ideal = sSup (Set.range fun (i : ι) ↦ (I i).ideal)
Tactic: rw [← sSup_range, ← sSup_range, ideal_sSup, ← Set.range_comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
rw : (sSup (Set.range I)).ideal = ⨆ (i : ι), (I i).ideal
rw₁ : (sSup (Set.range I)).ideal = sSup (Set.range fun (i : ι) ↦ (I i).ideal)
⊢ (iSup I).ideal = ⨆ (i : ι), (I i).ideal
have rw₂ : sSup (ideal '' Set.range I) = sSup (Set.range fun (i : ι) ↦ (I i).ideal)
Tactic: rw [← sSup_range, ← sSup_range, ideal_sSup, ← Set.range_comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
rw : (sSup (Set.range I)).ideal = ⨆ (i : ι), (I i).ideal
rw₁ : (sSup (Set.range I)).ideal = sSup (Set.range fun (i : ι) ↦ (I i).ideal)
rw₂ : sSup (ideal '' Set.range I) = sSup (Set.range fun (i : ι) ↦ (I i).ideal)
⊢ (iSup I).ideal = ⨆ (i : ι), (I i).ideal
have rw₃ : sSup (Set.range (ideal ∘ I)) = sSup (Set.range fun (i : ι) ↦ (I i).ideal)
Tactic: rw [← sSup_range, ← sSup_range, ideal_sSup, ← Set.range_comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
rw : (sSup (Set.range I)).ideal = ⨆ (i : ι), (I i).ideal
rw₁ : (sSup (Set.range I)).ideal = sSup (Set.range fun (i : ι) ↦ (I i).ideal)
rw₂ : sSup (ideal '' Set.range I) = sSup (Set.range fun (i : ι) ↦ (I i).ideal)
rw₃ : sSup (Set.range (ideal ∘ I)) = sSup (Set.range fun (i : ι) ↦ (I i).ideal)
⊢ (iSup I).ideal = ⨆ (i : ι), (I i).ideal
have rw₄ : Eq.{u + 1} (α := (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
  (sSup (Set.range fun (x : ι) ↦ (I x).ideal)) (sSup (Set.range fun (i : ι) ↦ (I i).ideal))
Tactic: rw [← sSup_range, ← sSup_range, ideal_sSup, ← Set.range_comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
s : Set ι
hs : s.Finite
⊢ Eq.{u + 1} (α := (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (ideal (⨅ i ∈ s, I i))
    (⨅ i ∈ s, (I i).ideal)
have refine : ∀ {i : ι} {s : Set ι} (his : i ∉ s) (hs : s.Finite)
  (e :
    Eq.{u + 1} (α := (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (ideal (⨅ i ∈ s, I i))
      (⨅ i ∈ s, (I i).ideal)),
  Eq.{u + 1} (α := (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
    (ideal (⨅ i_1 ∈ insert i s, I i_1)) (⨅ i_1 ∈ insert i s, (I i_1).ideal)
Tactic: refine hs.induction_on _ (by simp) fun {i s} his hs e ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
hV : V = X.affineBasicOpen f
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) = I.ideal V
have subst : Eq (α := Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
  (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op)) (I.ideal U)) (I.ideal (X.affineBasicOpen f))
Tactic: subst hV
Cleared hypotheses: V, hV
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
⊢ Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V) =
    I.ideal U
have rw : ∀ (x : ↥X) (h_1 : x ∈ (↑U : X.Opens)),
  Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (F :=
      (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x h_1))
      (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)))
    (Ideal.map (F := (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x h_1)) (I.ideal U))
Tactic: rw [U.2.ideal_ext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
x : ↥X
hxU : x ∈ (↑U : X.Opens)
⊢ Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (F :=
      (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU))
      (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)))
    (Ideal.map (F := (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU)) (I.ideal U))
have obtain : ∀ (f : (↑Γ(X, (↑U : X.Opens)) : Type u)) (g : (↑Γ(X, (↑V : X.Opens)) : Type u)) (hfg : X.basicOpen f = X.basicOpen g)
  (hxf : x ∈ X.basicOpen f),
  Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (F :=
      (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU))
      (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)))
    (Ideal.map (F := (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU)) (I.ideal U))
Tactic: obtain ⟨f, g, hfg, hxf⟩ := exists_basicOpen_le_affine_inter U.2 V.2 x ⟨hxU, h hxU⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
x : ↥X
hxU : x ∈ (↑U : X.Opens)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
g : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
⊢ Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (F :=
      (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU))
      (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)))
    (Ideal.map (F := (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU)) (I.ideal U))
have this : Eq (α := Ideal (↑Γ(X, (↑(X.affineBasicOpen g) : X.Opens)) : Type u))
  (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, (↑(X.affineBasicOpen g) : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))) (I.ideal U))
  (I.ideal (X.affineBasicOpen g))
Tactic: have := I.map_ideal_basicOpen_of_eq (V := X.affineBasicOpen g) f (Subtype.ext hfg.symm)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
x : ↥X
hxU : x ∈ (↑U : X.Opens)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
g : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this :
  Eq (α := Ideal (↑Γ(X, (↑(X.affineBasicOpen g) : X.Opens)) : Type u))
    (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, (↑(X.affineBasicOpen g) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) (I.ideal U))
    (I.ideal (X.affineBasicOpen g))
⊢ Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (F :=
      (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU))
      (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)))
    (Ideal.map (F := (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU)) (I.ideal U))
have this₁ : Eq (α := Ideal (↑Γ(X, (↑(X.affineBasicOpen g) : X.Opens)) : Type u))
  (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, (↑(X.affineBasicOpen g) : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))) (I.ideal U))
  (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op)) (I.ideal V))
Tactic: rw [← I.map_ideal_basicOpen] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
x : ↥X
hxU : x ∈ (↑U : X.Opens)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
g : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this :
  Eq (α := Ideal (↑Γ(X, (↑(X.affineBasicOpen g) : X.Opens)) : Type u))
    (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, (↑(X.affineBasicOpen g) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) (I.ideal U))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal V))
⊢ Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (F :=
      (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU))
      (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)))
    (Ideal.map (F := (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU)) (I.ideal U))
have this₁ : Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
  (Ideal.map (R := (↑(X.presheaf.obj (Opposite.op (X.basicOpen g))) : Type u)) (F :=
    (↑(X.presheaf.obj (Opposite.op (X.basicOpen g))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom (X.presheaf.germ (X.basicOpen g) x sorry))
    (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, (↑(X.affineBasicOpen g) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))) (I.ideal U)))
  (Ideal.map (R := (↑(X.presheaf.obj (Opposite.op (X.basicOpen g))) : Type u)) (F :=
    (↑(X.presheaf.obj (Opposite.op (X.basicOpen g))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom (X.presheaf.germ (X.basicOpen g) x sorry))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op)) (I.ideal V)))
Tactic: apply_fun Ideal.map (X.presheaf.germ (X.basicOpen g) x (hfg ▸ hxf)).hom at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
x : ↥X
hxU : x ∈ (↑U : X.Opens)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
g : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this :
  Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
    (Ideal.map (R := (↑(X.presheaf.obj (Opposite.op (X.basicOpen g))) : Type u)) (F :=
      (↑(X.presheaf.obj (Opposite.op (X.basicOpen g))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (X.basicOpen g) x ⋯))
      (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, (↑(X.affineBasicOpen g) : X.Opens)) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) (I.ideal U)))
    (Ideal.map (R := (↑(X.presheaf.obj (Opposite.op (X.basicOpen g))) : Type u)) (F :=
      (↑(X.presheaf.obj (Opposite.op (X.basicOpen g))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (X.basicOpen g) x ⋯))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal V)))
⊢ Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (F :=
      (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU))
      (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)))
    (Ideal.map (F := (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU)) (I.ideal U))
have simp : ∀
  (this :
    Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
      (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x sorry)) (I.ideal U))
      (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.germ (↑V : X.Opens) x sorry)) (I.ideal V))),
  Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
    (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op ≫ X.presheaf.germ (↑U : X.Opens) x hxU)) (I.ideal V))
    (Ideal.map (F := (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU)) (I.ideal U))
Tactic: simp only [Ideal.map_map, ← CommRingCat.hom_comp, affineBasicOpen_coe, X.presheaf.germ_res]
    at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
⊢ I.ideal V ≤
    Ideal.comap (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal U)
have rw : Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V) ≤
  I.ideal U
Tactic: rw [← Ideal.map_le_iff_le_comap, ← I.map_ideal h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
rw :
  Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V) ≤
    I.ideal U
⊢ I.ideal V ≤
    Ideal.comap (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal U)
have rw₁ : LE.le (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
  (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V))
  (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V))
Tactic: rw [← Ideal.map_le_iff_le_comap, ← I.map_ideal h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H : ∀ (i : ι), LE.le (α := Ideal (↑Γ(X, (↑(U i) : X.Opens)) : Type u)) (I.ideal (U i)) (J.ideal (U i))
V : (↑X.affineOpens : Type u)
x : ↥X
hxV : x ∈ (↑V : X.Opens)
⊢ ∃ (i : ι) (r : (↑Γ(X, (↑V : X.Opens)) : Type u)) (rU : (↑Γ(X, (↑(U i) : X.Opens)) : Type u)),
    X.basicOpen r = X.basicOpen rU ∧ (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ (↑V : X.Opens)) x hxV) : ↥X) ∈ X.basicOpen r
have obtain : ∀ (i : ι) (hi : x ∈ (↑(U i) : X.Opens)),
  ∃ (i : ι) (r : (↑Γ(X, (↑V : X.Opens)) : Type u)) (rU : (↑Γ(X, (↑(U i) : X.Opens)) : Type u)),
    X.basicOpen r = X.basicOpen rU ∧ (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ (↑V : X.Opens)) x hxV) : ↥X) ∈ X.basicOpen r
Tactic: obtain ⟨i, hi⟩ := TopologicalSpace.Opens.mem_iSup.mp (hU.ge (Set.mem_univ x))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
Goal:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H : ∀ (i : ι), LE.le (α := Ideal (↑Γ(X, (↑(U i) : X.Opens)) : Type u)) (I.ideal (U i)) (J.ideal (U i))
V : (↑X.affineOpens : Type u)
⊢ I.ideal V ≤ J.ideal V
have this : ∀ (x : ↥(↑V : X.Opens)),
  ∃ (i : ι) (r : (↑Γ(X, (↑V : X.Opens)) : Type u)) (rU : (↑Γ(X, (↑(U i) : X.Opens)) : Type u)),
    X.basicOpen r = X.basicOpen rU ∧ (↑x : ↥X) ∈ X.basicOpen r
Tactic: have : ∀ x : V.1, ∃ (i : ι) (r : Γ(X, V.1)) (rU : Γ(X, U i)),
      X.basicOpen r = X.basicOpen rU ∧ x.1 ∈ X.basicOpen r := by
    intro ⟨x, hxV⟩
    obtain ⟨i, hi⟩ := TopologicalSpace.Opens.mem_iSup.mp (hU.ge (Set.mem_univ x))
    exact ⟨i, exists_basicOpen_le_affine_inter V.2 (U i).2 _ ⟨hxV, hi⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H : ∀ (i : ι), LE.le (α := Ideal (↑Γ(X, (↑(U i) : X.Opens)) : Type u)) (I.ideal (U i)) (J.ideal (U i))
V : (↑X.affineOpens : Type u)
this :
  ∀ (x : ↥(↑V : X.Opens)),
    ∃ (i : ι) (r : (↑Γ(X, (↑V : X.Opens)) : Type u)) (rU : (↑Γ(X, (↑(U i) : X.Opens)) : Type u)),
      X.basicOpen r = X.basicOpen rU ∧ (↑x : ↥X) ∈ X.basicOpen r
⊢ I.ideal V ≤ J.ideal V
have choose : ∀ (i : (x : ↥(↑V : X.Opens)) → ι) (r : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u))
  (rU : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑(U (i x)) : X.Opens)) : Type u))
  (e : ∀ (x : ↥(↑V : X.Opens)), X.basicOpen (r x) = X.basicOpen (rU x))
  (hxr : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (r x)), I.ideal V ≤ J.ideal V
Tactic: choose i r rU e hxr using this
Cleared hypotheses: this