awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
A : Type v
inst_2 : CommRing A
f : R →+* A
rw : (↑(W.map f).Δ'⁻¹ : A) * HPow.hPow (β := ℕ) (W.map f).c₄ 3 = (f : (a : R) → A) W.j
rw₁ :
  HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A) (HPow.hPow (β := ℕ) (W.map f).c₄ 3) = (f : (a : R) → A) W.j
⊢ (W.map f).j = (f : (a : R) → A) W.j
have rw₂ : HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A) (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.c₄ : A) 3) =
  (f : (a : R) → A) W.j
Tactic: rw [j, coe_inv_map_Δ', map_c₄, j, map_mul, map_pow]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
A : Type v
inst_2 : CommRing A
f : R →+* A
rw : (↑(W.map f).Δ'⁻¹ : A) * HPow.hPow (β := ℕ) (W.map f).c₄ 3 = (f : (a : R) → A) W.j
rw₁ :
  HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A) (HPow.hPow (β := ℕ) (W.map f).c₄ 3) = (f : (a : R) → A) W.j
rw₂ :
  HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A)
      (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.c₄ : A) 3) =
    (f : (a : R) → A) W.j
⊢ (W.map f).j = (f : (a : R) → A) W.j
have rw₃ : HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A) (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.c₄ : A) 3) =
  (f : (a : R) → A) ((↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3)
Tactic: rw [j, coe_inv_map_Δ', map_c₄, j, map_mul, map_pow]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
A : Type v
inst_2 : CommRing A
f : R →+* A
rw : (↑(W.map f).Δ'⁻¹ : A) * HPow.hPow (β := ℕ) (W.map f).c₄ 3 = (f : (a : R) → A) W.j
rw₁ :
  HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A) (HPow.hPow (β := ℕ) (W.map f).c₄ 3) = (f : (a : R) → A) W.j
rw₂ :
  HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A)
      (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.c₄ : A) 3) =
    (f : (a : R) → A) W.j
rw₃ :
  HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A)
      (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.c₄ : A) 3) =
    (f : (a : R) → A) ((↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3)
⊢ (W.map f).j = (f : (a : R) → A) W.j
have rw₄ : HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A) (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.c₄ : A) 3) =
  HMul.hMul (α := A) (β := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A) ((f : (a : R) → A) (HPow.hPow (β := ℕ) W.c₄ 3) : A)
Tactic: rw [j, coe_inv_map_Δ', map_c₄, j, map_mul, map_pow]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsElliptic
A : Type v
inst_2 : CommRing A
f : R →+* A
rw : (↑(W.map f).Δ'⁻¹ : A) * HPow.hPow (β := ℕ) (W.map f).c₄ 3 = (f : (a : R) → A) W.j
rw₁ :
  HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A) (HPow.hPow (β := ℕ) (W.map f).c₄ 3) = (f : (a : R) → A) W.j
rw₂ :
  HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A)
      (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.c₄ : A) 3) =
    (f : (a : R) → A) W.j
rw₃ :
  HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A)
      (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.c₄ : A) 3) =
    (f : (a : R) → A) ((↑W.Δ'⁻¹ : R) * HPow.hPow (β := ℕ) W.c₄ 3)
rw₄ :
  HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A)
      (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.c₄ : A) 3) =
    HMul.hMul (α := A) (β := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A)
      ((f : (a : R) → A) (HPow.hPow (β := ℕ) W.c₄ 3) : A)
⊢ (W.map f).j = (f : (a : R) → A) W.j
have rw₅ : HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A) (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.c₄ : A) 3) =
  HMul.hMul (α := A) ((f : (a : R) → A) (↑W.Δ'⁻¹ : R) : A) (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.c₄ : A) 3)
Tactic: rw [j, coe_inv_map_Δ', map_c₄, j, map_mul, map_pow]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Fiber (goal)
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ IsPullback
    (pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
      (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯)
    (Scheme.Hom.fiberToSpecResidueField snd y) (Scheme.Hom.fiberToSpecResidueField f (g y))
    (Spec.map (Scheme.Hom.residueFieldMap g y))
have refine_1 : IsPullback
  (CategoryStruct.comp (Y := pullback (Y := Spec (Z.residueField (g y))) f (Z.fromSpecResidueField (g y)))
    (pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
      (Spec.map (Scheme.Hom.residueFieldMap g y)) g sorry sorry)
    (pullback.fst f (Z.fromSpecResidueField (g y))))
  (Scheme.Hom.fiberToSpecResidueField snd y) f
  (Spec.map (Scheme.Hom.residueFieldMap g y) ≫ Z.fromSpecResidueField (g y))
Tactic: refine .of_right (h₁₂ := pullback.fst _ _) ?_ ?_
      (IsPullback.of_hasPullback f (Z.fromSpecResidueField (g y)))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Fiber (goal)
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
refine_1 :
  IsPullback
    (CategoryStruct.comp (Y := pullback (Y := Spec (Z.residueField (g y))) f (Z.fromSpecResidueField (g y)))
      (pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
        (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯)
      (pullback.fst f (Z.fromSpecResidueField (g y))))
    (Scheme.Hom.fiberToSpecResidueField snd y) f
    (Spec.map (Scheme.Hom.residueFieldMap g y) ≫ Z.fromSpecResidueField (g y))
⊢ IsPullback
    (pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
      (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯)
    (Scheme.Hom.fiberToSpecResidueField snd y) (Scheme.Hom.fiberToSpecResidueField f (g y))
    (Spec.map (Scheme.Hom.residueFieldMap g y))
have refine_2 : pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
      (Spec.map (Scheme.Hom.residueFieldMap g y)) g sorry sorry ≫
    Scheme.Hom.fiberToSpecResidueField f (g y) =
  Scheme.Hom.fiberToSpecResidueField snd y ≫ Spec.map (Scheme.Hom.residueFieldMap g y)
Tactic: refine .of_right (h₁₂ := pullback.fst _ _) ?_ ?_
      (IsPullback.of_hasPullback f (Z.fromSpecResidueField (g y)))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Fiber (goal)
Goal:
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
⊢ Arrow.mk (X := Scheme.Hom.fiber (X := Spec (CommRingCat.of S)) (map (CommRingCat.ofHom (algebraMap R S))) p)
      (Scheme.Hom.fiberToSpecResidueField (map (CommRingCat.ofHom (algebraMap R S))) p) ≅
    Arrow.mk (X := Spec (CommRingCat.of (p.asIdeal.Fiber S))) (Y := Spec (CommRingCat.of p.asIdeal.ResidueField))
      (map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))))
have refine_1 : pullback (X := Spec ((Spec (CommRingCat.of R)).residueField p)) (Y := Spec (CommRingCat.of S))
    ((Spec (CommRingCat.of R)).fromSpecResidueField p) (map (CommRingCat.ofHom (algebraMap R S))) ≅
  pullback (X := Spec (CommRingCat.of p.asIdeal.ResidueField)) (Y := Spec (CommRingCat.of S)) (Z :=
    Spec (CommRingCat.of R)) (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
    (map (CommRingCat.ofHom (algebraMap R S)))
Tactic: refine Arrow.isoMk' _ _
    (pullbackSymmetry _ _ ≪≫ ?_ ≪≫ pullbackSpecIso R p.asIdeal.ResidueField S) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Fiber (goal)
Goal:
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
refine_1 :
  pullback (X := Spec ((Spec (CommRingCat.of R)).residueField p)) (Y := Spec (CommRingCat.of S))
      ((Spec (CommRingCat.of R)).fromSpecResidueField p) (map (CommRingCat.ofHom (algebraMap R S))) ≅
    pullback (X := Spec (CommRingCat.of p.asIdeal.ResidueField)) (Y := Spec (CommRingCat.of S)) (Z :=
      Spec (CommRingCat.of R)) (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
      (map (CommRingCat.ofHom (algebraMap R S)))
⊢ Arrow.mk (X := Scheme.Hom.fiber (X := Spec (CommRingCat.of S)) (map (CommRingCat.ofHom (algebraMap R S))) p)
      (Scheme.Hom.fiberToSpecResidueField (map (CommRingCat.ofHom (algebraMap R S))) p) ≅
    Arrow.mk (X := Spec (CommRingCat.of (p.asIdeal.Fiber S))) (Y := Spec (CommRingCat.of p.asIdeal.ResidueField))
      (map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))))
have refine_2 : Spec ((Spec (CommRingCat.of R)).residueField p) ≅ Spec (CommRingCat.of p.asIdeal.ResidueField)
Tactic: refine Arrow.isoMk' _ _
    (pullbackSymmetry _ _ ≪≫ ?_ ≪≫ pullbackSpecIso R p.asIdeal.ResidueField S) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Fiber (goal)
Goal:
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
refine_1 :
  pullback (X := Spec ((Spec (CommRingCat.of R)).residueField p)) (Y := Spec (CommRingCat.of S))
      ((Spec (CommRingCat.of R)).fromSpecResidueField p) (map (CommRingCat.ofHom (algebraMap R S))) ≅
    pullback (X := Spec (CommRingCat.of p.asIdeal.ResidueField)) (Y := Spec (CommRingCat.of S)) (Z :=
      Spec (CommRingCat.of R)) (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
      (map (CommRingCat.ofHom (algebraMap R S)))
refine_2 : Spec ((Spec (CommRingCat.of R)).residueField p) ≅ Spec (CommRingCat.of p.asIdeal.ResidueField)
⊢ Arrow.mk (X := Scheme.Hom.fiber (X := Spec (CommRingCat.of S)) (map (CommRingCat.ofHom (algebraMap R S))) p)
      (Scheme.Hom.fiberToSpecResidueField (map (CommRingCat.ofHom (algebraMap R S))) p) ≅
    Arrow.mk (X := Spec (CommRingCat.of (p.asIdeal.Fiber S))) (Y := Spec (CommRingCat.of p.asIdeal.ResidueField))
      (map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))))
have refine_3 : Eq (α :=
  Scheme.Hom.fiber (X := Spec (CommRingCat.of S)) (map (CommRingCat.ofHom (algebraMap R S))) p ⟶
    Spec (CommRingCat.of p.asIdeal.ResidueField))
  (Iso.hom
      (pullbackSymmetry (map (CommRingCat.ofHom (algebraMap R S))) ((Spec (CommRingCat.of R)).fromSpecResidueField p) ≪≫
        Iso.trans (Y :=
            pullback (X := Spec ((Spec (CommRingCat.of R)).residueField p)) (Y := Spec (CommRingCat.of S)) (Z :=
              Spec (CommRingCat.of R))
              (map (Iso.inv (Scheme.Spec.residueFieldIso (CommRingCat.of R) p)) ≫
                map (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of R) : Type u) p.asIdeal.ResidueField)))
              (map (CommRingCat.ofHom (algebraMap R S))))
            (pullback.congrHom sorry sorry)
            (asIso
              (pullback.map
                (map (Iso.inv (Scheme.Spec.residueFieldIso (CommRingCat.of R) p)) ≫
                  map (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of R) : Type u) p.asIdeal.ResidueField)))
                (map (CommRingCat.ofHom (algebraMap R S)))
                (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
                (map (CommRingCat.ofHom (algebraMap R S)))
                (map (Iso.inv (Scheme.Spec.residueFieldIso (CommRingCat.of R) p))) (𝟙 (Spec (CommRingCat.of S)))
                (𝟙 (Spec (CommRingCat.of R))) sorry sorry)) ≪≫
          pullbackSpecIso R p.asIdeal.ResidueField S) ≫
    map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))))
  (Scheme.Hom.fiberToSpecResidueField (map (CommRingCat.ofHom (algebraMap R S))) p ≫
    Iso.hom (Scheme.Spec.mapIso (Iso.op (Iso.symm (Scheme.Spec.residueFieldIso (CommRingCat.of R) p)))))
Tactic: refine Arrow.isoMk' _ _
    (pullbackSymmetry _ _ ≪≫ ?_ ≪≫ pullbackSpecIso R p.asIdeal.ResidueField S) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Fiber (goal)
Goal:
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
⊢ pullback (X := Spec ((Spec (CommRingCat.of R)).residueField p)) (Y := Spec (CommRingCat.of S))
      ((Spec (CommRingCat.of R)).fromSpecResidueField p) (map (CommRingCat.ofHom (algebraMap R S))) ≅
    pullback (X := Spec (CommRingCat.of p.asIdeal.ResidueField)) (Y := Spec (CommRingCat.of S)) (Z :=
      Spec (CommRingCat.of R)) (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
      (map (CommRingCat.ofHom (algebraMap R S)))
have refine_1 : pullback (X := Spec ((Spec (CommRingCat.of R)).residueField p)) (Y := Spec (CommRingCat.of S)) (Z :=
    Spec (CommRingCat.of R))
    (map (Iso.inv (Scheme.Spec.residueFieldIso (CommRingCat.of R) p)) ≫
      map (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of R) : Type u) p.asIdeal.ResidueField)))
    (map (CommRingCat.ofHom (algebraMap R S))) ≅
  pullback (X := Spec (CommRingCat.of p.asIdeal.ResidueField)) (Y := Spec (CommRingCat.of S)) (Z :=
    Spec (CommRingCat.of R)) (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
    (map (CommRingCat.ofHom (algebraMap R S)))
Tactic: refine pullback.congrHom
      (Scheme.Spec.map_residueFieldIso_inv_eq_fromSpecResidueField (.of R) p).symm rfl ≪≫ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
⊢ Function.Injective (α := (↑(X.presheaf.obj (op U)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx)) :
      (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
have rw : ∀ (a : (↑(X.presheaf.obj (op U)) : Type u_1)),
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          a :
        (↑(X.presheaf.stalk x) : Type u_1))
      (0 : (↑(X.presheaf.stalk x) : Type u_1)) →
    a = 0
Tactic: rw [injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (hypothesis)
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
y : (↑(X.presheaf.obj (op U)) : Type u_1)
hy :
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        y :
      (↑(X.presheaf.stalk x) : Type u_1))
    (0 : (↑(X.presheaf.stalk x) : Type u_1))
⊢ y = 0
have hy₁ : Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
        (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
      y :
    (↑(X.presheaf.stalk x) : Type u_1))
  ((CommRingCat.Hom.hom (X.presheaf.germ U x hx) :
        (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
      0 :
    (↑(X.presheaf.stalk x) : Type u_1))
Tactic: rw [← (X.presheaf.germ U x hx).hom.map_zero] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
y : (↑(X.presheaf.obj (op U)) : Type u_1)
hy :
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        y :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))
⊢ y = 0
have obtain : ∀ (W : Opens ↥X) (hW : x ∈ W) (iU iV : W ⟶ U)
  (e :
    Eq (α := (↑(X.presheaf.obj (op W)) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.map iU.op) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
          y :
        (↑(X.presheaf.obj (op W)) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.map iV.op) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
          0 :
        (↑(X.presheaf.obj (op W)) : Type u_1))),
  y = 0
Tactic: obtain ⟨W, hW, iU, iV, e⟩ := X.presheaf.germ_eq _ hx hx _ _ hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (hypothesis)
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
y : (↑(X.presheaf.obj (op U)) : Type u_1)
hy :
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        y :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))
W : Opens ↥X
hW : x ∈ W
iU iV : W ⟶ U
e :
  Eq (α := (↑(X.presheaf.obj (op W)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iU.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
        y :
      (↑(X.presheaf.obj (op W)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iV.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
        0 :
      (↑(X.presheaf.obj (op W)) : Type u_1))
⊢ y = 0
have e₁ : Eq (α := (↑(X.presheaf.obj (op W)) : Type u_1))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (X.presheaf.map iU.op) :
        (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
      y :
    (↑(X.presheaf.obj (op W)) : Type u_1))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (X.presheaf.map iU.op) :
        (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
      0 :
    (↑(X.presheaf.obj (op W)) : Type u_1))
Tactic: cases Subsingleton.elim iU iV
Cleared hypotheses: iV, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (hypothesis)
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
y : (↑(X.presheaf.obj (op U)) : Type u_1)
hy :
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        y :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))
W : Opens ↥X
hW : x ∈ W
iU : W ⟶ U
e :
  Eq (α := (↑(X.presheaf.obj (op W)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iU.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
        y :
      (↑(X.presheaf.obj (op W)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iU.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
        0 :
      (↑(X.presheaf.obj (op W)) : Type u_1))
⊢ y = 0
have this : Nonempty.{u_1 + 1} ↥(↑W : Scheme)
Tactic: haveI : Nonempty W := ⟨⟨_, hW⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
⊢ Eq (α := ↥Y) (f (genericPoint ↥X) : ↥Y) (genericPoint ↥Y : ↥Y)
have apply : IsGenericPoint (α := ↥Y) (f (genericPoint ↥X) : ↥Y) (Set.univ : Set ↥Y)
Tactic: apply ((genericPoint_spec Y).eq _).symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
⊢ IsGenericPoint (α := ↥Y) (f (genericPoint ↥X) : ↥Y) (Set.univ : Set ↥Y)
have h : Eq (α := Set ↥Y) Set.univ (closure (Set.image (α := ↥X) (⇑f) Set.univ))
Tactic: convert! (genericPoint_spec X).image f.continuous
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
⊢ Eq (α := Set ↥Y) Set.univ (closure (Set.image (α := ↥X) (⇑f) Set.univ))
have h : Eq (α := Set ↥Y) (closure (Set.image (α := ↥X) (⇑f) Set.univ)) Set.univ
Tactic: symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
⊢ Eq (α := Set ↥Y) (closure (Set.image (α := ↥X) (⇑f) Set.univ)) Set.univ
have h : Subset (α := Set ↥Y) Set.univ (closure (Set.image (α := ↥X) (⇑f) Set.univ))
Tactic: rw [← Set.univ_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
⊢ Subset (α := Set ↥Y) Set.univ (closure (Set.image (α := ↥X) (⇑f) Set.univ))
have h : Eq (α := Set ↥Y) (Set.image (α := ↥X) (⇑f) Set.univ) (Set.univ ∩ Set.range (ι := ↥X) ⇑f)
Tactic: convert! subset_closure_inter_of_isPreirreducible_of_isOpen _ f.isOpenEmbedding.isOpen_range _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
h : Eq (α := Set ↥Y) (Set.image (α := ↥X) (⇑f) Set.univ) (Set.univ ∩ Set.range (ι := ↥X) ⇑f)
⊢ Subset (α := Set ↥Y) Set.univ (closure (Set.image (α := ↥X) (⇑f) Set.univ))
have h₁ : IsPreirreducible.{u_1} (X := ↥Y) Set.univ
Tactic: convert! subset_closure_inter_of_isPreirreducible_of_isOpen _ f.isOpenEmbedding.isOpen_range _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.FunctionField (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
h : Eq (α := Set ↥Y) (Set.image (α := ↥X) (⇑f) Set.univ) (Set.univ ∩ Set.range (ι := ↥X) ⇑f)
h₁ : IsPreirreducible.{u_1} (X := ↥Y) Set.univ
⊢ Subset (α := Set ↥Y) Set.univ (closure (Set.image (α := ↥X) (⇑f) Set.univ))
have h₂ : Set.Nonempty (α := ↥Y) (Set.univ ∩ Set.range (ι := ↥X) ⇑f)
Tactic: convert! subset_closure_inter_of_isPreirreducible_of_isOpen _ f.isOpenEmbedding.isOpen_range _