awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
xk : ↥(d.functor.obj k)
h2 : (d.natTrans.app k) xk = uk
h_1 :
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor))
h_2 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) :
      ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
h :
  Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
    (d.toBase ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor)) : ↥S)
⊢ Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))
    ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor))
have h₁ : Eq (α := ↥(colimit d.functor))
  ((colimit.ι d.functor i) ((d.functor.map fi) xk : ↥(d.functor.obj i)) : ↥(colimit d.functor))
  ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor))
Tactic: use d.functor.map fi xk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
y : ↥(d.functor.obj i)
⊢ Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor i) y : ↥(colimit d.functor))
have h : Eq (α := ↥S)
  ((𝒰.f i)
      ((d.natTrans.app i) y :
        ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)) :
    ↥S)
  (d.toBase ((colimit.ι d.functor i) y : ↥(colimit d.functor)) : ↥S)
Tactic: use d.natTrans.app i y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
y : ↥(d.functor.obj i)
⊢ Eq (α := ↥S)
    ((𝒰.f i)
        ((d.natTrans.app i) y :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)) :
      ↥S)
    (d.toBase ((colimit.ι d.functor i) y : ↥(colimit d.functor)) : ↥S)
have h : Eq (α := ↥S)
  ((𝒰.f i)
      ((d.natTrans.app i) y :
        ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)) :
    ↥S)
  ((d.natTrans.app i ≫ 𝒰.f i) y : ↥S)
Tactic: rw [← Scheme.Hom.comp_apply, ι_toBase]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
⊢ IsPullback (Y := colimit d.functor) (d.natTrans.app i) (colimit.ι d.functor i : d.functor.obj i ⟶ colimit d.functor)
    (𝒰.f i) (d.toBase : d.glued ⟶ S)
have refine_1 : (s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)) → s.pt ⟶ d.functor.obj i
Tactic: refine ⟨by simp, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
refine_1 : (s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)) → s.pt ⟶ d.functor.obj i
⊢ IsPullback (Y := colimit d.functor) (d.natTrans.app i) (colimit.ι d.functor i : d.functor.obj i ⟶ colimit d.functor)
    (𝒰.f i) (d.toBase : d.glued ⟶ S)
have refine_2 : ∀ (s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)),
  IsOpenImmersion.lift (colimit.ι d.functor i) s.snd sorry ≫ d.natTrans.app i = s.fst
Tactic: refine ⟨by simp, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
refine_1 : (s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)) → s.pt ⟶ d.functor.obj i
refine_2 :
  ∀ (s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)),
    IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i = s.fst
⊢ IsPullback (Y := colimit d.functor) (d.natTrans.app i) (colimit.ι d.functor i : d.functor.obj i ⟶ colimit d.functor)
    (𝒰.f i) (d.toBase : d.glued ⟶ S)
have refine_3 : ∀ (s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)),
  IsOpenImmersion.lift (colimit.ι d.functor i) s.snd sorry ≫ colimit.ι d.functor i = s.snd
Tactic: refine ⟨by simp, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
refine_1 : (s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)) → s.pt ⟶ d.functor.obj i
refine_2 :
  ∀ (s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)),
    IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i = s.fst
refine_3 :
  ∀ (s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)),
    IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ colimit.ι d.functor i = s.snd
⊢ IsPullback (Y := colimit d.functor) (d.natTrans.app i) (colimit.ι d.functor i : d.functor.obj i ⟶ colimit d.functor)
    (𝒰.f i) (d.toBase : d.glued ⟶ S)
have refine_4 : ∀ (s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)) (m : s.pt ⟶ d.functor.obj i),
  m ≫ d.natTrans.app i = s.fst →
    m ≫ colimit.ι d.functor i = s.snd → m = IsOpenImmersion.lift (colimit.ι d.functor i) s.snd sorry
Tactic: refine ⟨by simp, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)
⊢ s.pt ⟶ d.functor.obj i
have refine_1 : Subset (α := Set ↥(colimit d.functor)) (Set.range (ι := ↥s.pt) ⇑s.snd)
  (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))
Tactic: apply IsOpenImmersion.lift (colimit.ι d.functor i) s.snd
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)
⊢ Subset (α := Set ↥(colimit d.functor)) (Set.range (ι := ↥s.pt) ⇑s.snd)
    (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))
have refine_1 : Subset (α := Set ↥(colimit d.functor)) (Set.range (ι := ↥s.pt) ⇑s.snd)
  (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
Tactic: rw [← preimage_toBase_eq_range_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)
x : ↥s.pt
⊢ Membership.mem (α := ↥(colimit d.functor)) (γ := Set ↥(colimit d.functor))
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))) (s.snd x : ↥(colimit d.functor))
have h : Eq (α := ↥S)
  ((𝒰.f i) (s.fst x : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)) : ↥S)
  (d.toBase (s.snd x : ↥(colimit d.functor)) : ↥S)
Tactic: use s.fst x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)
x : ↥s.pt
⊢ Eq (α := ↥S)
    ((𝒰.f i) (s.fst x : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)) : ↥S)
    (d.toBase (s.snd x : ↥(colimit d.functor)) : ↥S)
have h : Eq (α := ↥S)
  ((𝒰.f i) (s.fst x : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)) : ↥S)
  ((s.fst ≫ 𝒰.f i) x : ↥S)
Tactic: rw [← Scheme.Hom.comp_apply, ← s.condition]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)
⊢ IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i = s.fst
have refine_2 : (IsOpenImmersion.lift (colimit.ι d.functor i) s.snd sorry ≫ d.natTrans.app i) ≫ 𝒰.f i = s.fst ≫ 𝒰.f i
Tactic: rw [← cancel_mono (𝒰.f i), Category.assoc, ← ι_toBase, IsOpenImmersion.lift_fac_assoc,
      s.condition]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)
refine_2 : (IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i) ≫ 𝒰.f i = s.fst ≫ 𝒰.f i
⊢ IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i = s.fst
have refine_2₁ : IsOpenImmersion.lift (colimit.ι d.functor i) s.snd sorry ≫ d.natTrans.app i ≫ 𝒰.f i = s.fst ≫ 𝒰.f i
Tactic: rw [← cancel_mono (𝒰.f i), Category.assoc, ← ι_toBase, IsOpenImmersion.lift_fac_assoc,
      s.condition]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)
refine_2 : (IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i) ≫ 𝒰.f i = s.fst ≫ 𝒰.f i
refine_2₁ : IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i ≫ 𝒰.f i = s.fst ≫ 𝒰.f i
⊢ IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i = s.fst
have refine_2₂ : IsOpenImmersion.lift (colimit.ι d.functor i) s.snd sorry ≫
    CategoryStruct.comp (Y := colimit d.functor) (colimit.ι d.functor i : d.functor.obj i ⟶ colimit d.functor)
      (d.toBase : d.glued ⟶ S) =
  s.fst ≫ 𝒰.f i
Tactic: rw [← cancel_mono (𝒰.f i), Category.assoc, ← ι_toBase, IsOpenImmersion.lift_fac_assoc,
      s.condition]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)
refine_2 : (IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i) ≫ 𝒰.f i = s.fst ≫ 𝒰.f i
refine_2₁ : IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i ≫ 𝒰.f i = s.fst ≫ 𝒰.f i
refine_2₂ :
  IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫
      CategoryStruct.comp (Y := colimit d.functor) (colimit.ι d.functor i : d.functor.obj i ⟶ colimit d.functor)
        (d.toBase : d.glued ⟶ S) =
    s.fst ≫ 𝒰.f i
⊢ IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i = s.fst
have refine_2₃ : s.snd ≫ d.toBase = s.fst ≫ 𝒰.f i
Tactic: rw [← cancel_mono (𝒰.f i), Category.assoc, ← ι_toBase, IsOpenImmersion.lift_fac_assoc,
      s.condition]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)
refine_2 : (IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i) ≫ 𝒰.f i = s.fst ≫ 𝒰.f i
refine_2₁ : IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i ≫ 𝒰.f i = s.fst ≫ 𝒰.f i
refine_2₂ :
  IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫
      CategoryStruct.comp (Y := colimit d.functor) (colimit.ι d.functor i : d.functor.obj i ⟶ colimit d.functor)
        (d.toBase : d.glued ⟶ S) =
    s.fst ≫ 𝒰.f i
refine_2₃ : s.snd ≫ d.toBase = s.fst ≫ 𝒰.f i
⊢ IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i = s.fst
have refine_2₄ : s.snd ≫ d.toBase = s.snd ≫ d.toBase
Tactic: rw [← cancel_mono (𝒰.f i), Category.assoc, ← ι_toBase, IsOpenImmersion.lift_fac_assoc,
      s.condition]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
X_1 : Scheme
U : X_1.Opens
X Y : Scheme
f : X ⟶ Y
x y : ↥X
h : x = y
⊢ X.residueField x = X.residueField y
have subst : X.residueField x = X.residueField x
Tactic: subst h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
X : Scheme
x y z : ↥X
e : x = y
e' : y = z
⊢ residueFieldCongr e ≪≫ residueFieldCongr e' = residueFieldCongr ⋯
have subst : residueFieldCongr sorry ≪≫ residueFieldCongr sorry = residueFieldCongr sorry
Tactic: subst e e'
Cleared hypotheses: y, z, e, e'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
X : Scheme
x y z : ↥X
e : x = y
e' : y = z
⊢ (residueFieldCongr e).hom ≫ (residueFieldCongr e').hom = (residueFieldCongr ⋯).hom
have subst : (residueFieldCongr sorry).hom ≫ (residueFieldCongr sorry).hom = (residueFieldCongr sorry).hom
Tactic: subst e e'
Cleared hypotheses: y, z, e, e'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
X : Scheme
x y : ↥X
h : x = y
⊢ X.residue x ≫ (residueFieldCongr h).hom = Iso.hom (X.presheaf.stalkCongr ⋯) ≫ X.residue y
have subst : X.residue x ≫ (residueFieldCongr sorry).hom = Iso.hom (X.presheaf.stalkCongr sorry) ≫ X.residue x
Tactic: subst h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
X_1 : Scheme
U : X_1.Opens
X Y : Scheme
f_1 f g : X ⟶ Y
e : f = g
x : ↥X
⊢ Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
have subst : Eq (α := ↥Y) (f x : ↥Y) (f x : ↥Y)
Tactic: subst e
Cleared hypotheses: g, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
X Y : Scheme
f g : X ⟶ Y
e : f = g
x : ↥X
⊢ residueFieldMap f x = (residueFieldCongr ⋯).hom ≫ residueFieldMap g x
have subst : residueFieldMap f x = (residueFieldCongr sorry).hom ≫ residueFieldMap f x
Tactic: subst e
Cleared hypotheses: g, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
X_1 : Scheme
U : X_1.Opens
X_2 Y : Scheme
f : X_2 ⟶ Y
X : Scheme
x : ↥X
⊢ IsPreimmersion (Spec.map (X.residue x) ≫ X.fromSpecStalk x)
have rw : IsPreimmersion (Spec.map (X.residue x))
Tactic: rw [IsPreimmersion.comp_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
X : Scheme
x y : ↥X
h : x = y
⊢ Spec.map (residueFieldCongr h).hom ≫ X.fromSpecResidueField x = X.fromSpecResidueField y
have subst : Spec.map (residueFieldCongr sorry).hom ≫ X.fromSpecResidueField x = X.fromSpecResidueField x
Tactic: subst h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Spec.map (residueFieldMap f x) ≫ Spec.map (Y.residue (f x)) ≫ Y.fromSpecStalk (f x) =
    (Spec.map (X.residue x) ≫ X.fromSpecStalk x) ≫ f
have rw : Spec.map (Y.residue (f x) ≫ residueFieldMap f x) ≫ Y.fromSpecStalk (f x) =
  Spec.map (stalkMap f x ≫ X.residue x) ≫ Y.fromSpecStalk (f x)
Tactic: rw [Category.assoc, ← SpecMap_stalkMap_fromSpecStalk, ← Spec.map_comp_assoc,
    ← Spec.map_comp_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
K : Type u
inst : Field K
X : Scheme
f : Spec (CommRingCat.of K) ⟶ X
⊢ CategoryStruct.comp (Y := Spec (X.residueField (f (closedPoint (↑(CommRingCat.of K) : Type u)))))
      (Spec.map (descResidueField (stalkClosedPointTo f))) (X.fromSpecResidueField (f (closedPoint K))) =
    f
have rw : CategoryStruct.comp (Y := Spec (X.presheaf.stalk (f (closedPoint (↑(CommRingCat.of K) : Type u)))))
    (Spec.map (stalkClosedPointTo f)) (X.fromSpecStalk (f (closedPoint (↑(CommRingCat.of K) : Type u)))) =
  f
Tactic: rw [X.descResidueField_fromSpecResidueField, Scheme.Spec_stalkClosedPointTo_fromSpecStalk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
K : Type u
inst : Field K
X : Scheme
f : Spec (CommRingCat.of K) ⟶ X
rw :
  CategoryStruct.comp (Y := Spec (X.presheaf.stalk (f (closedPoint (↑(CommRingCat.of K) : Type u)))))
      (Spec.map (stalkClosedPointTo f)) (X.fromSpecStalk (f (closedPoint (↑(CommRingCat.of K) : Type u)))) =
    f
⊢ CategoryStruct.comp (Y := Spec (X.residueField (f (closedPoint (↑(CommRingCat.of K) : Type u)))))
      (Spec.map (descResidueField (stalkClosedPointTo f))) (X.fromSpecResidueField (f (closedPoint K))) =
    f
have rw₁ : f = f
Tactic: rw [X.descResidueField_fromSpecResidueField, Scheme.Spec_stalkClosedPointTo_fromSpecStalk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
R : CommRingCat
x : ↥(Spec R)
⊢ CommRingCat.ofHom (algebraMap (↑R : Type u_1) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv =
    (ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial ≫ (Spec R).residue x
have rw : Eq (α := CommRingCat.of (↑R : Type u_1) ⟶ (Spec R).residueField x)
  (CommRingCat.ofHom (algebraMap (↑R : Type u_1) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv)
  (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.AtPrime x.asIdeal)) ≫
    (Spec.stalkIso R x).inv ≫ (Spec R).residue x)
Tactic: rw [← Spec.algebraMap_stalkIso_inv_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
R : CommRingCat
x : ↥(Spec R)
⊢ Spec.map (residueFieldIso R x).inv ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) x.asIdeal.ResidueField)) =
    (Spec R).fromSpecResidueField x
have simp : Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv) =
  Spec.map (((ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial) ≫ (Spec R).residue x)
Tactic: simp only [Scheme.fromSpecResidueField, Spec.fromSpecStalk_eq, ← Spec.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
R : CommRingCat
x : ↥(Spec R)
⊢ Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv) =
    Spec.map (((ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial) ≫ (Spec R).residue x)
have rw : CommRingCat.ofHom (algebraMap (↑R : Type u_1) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv =
  ((ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial) ≫ (Spec R).residue x
Tactic: rw [Spec.map_inj]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
K : Type u_1
inst : Field K
X : Scheme
f₁ f₂ : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
⊢ f₁ = f₂ ↔
    ∃ (e :
      f₁.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
        f₂.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
      f₁.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
        (residueFieldCongr e).hom ≫ f₂.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
have mp : f₁ = f₂ →
  ∃ (e :
    f₁.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
      f₂.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
    f₁.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
      (residueFieldCongr e).hom ≫ f₂.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
K : Type u_1
inst : Field K
X : Scheme
f₁ f₂ : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
mp :
  f₁ = f₂ →
    ∃ (e :
      f₁.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
        f₂.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
      f₁.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
        (residueFieldCongr e).hom ≫ f₂.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
⊢ f₁ = f₂ ↔
    ∃ (e :
      f₁.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
        f₂.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
      f₁.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
        (residueFieldCongr e).hom ≫ f₂.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
have mpr : (∃ (e :
    f₁.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
      f₂.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
    f₁.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
      (residueFieldCongr e).hom ≫ f₂.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) →
  f₁ = f₂
Tactic: constructor