awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
j : I
Z : (i : I) → (i ⟶ j) → Set ↥(D.obj i)
hZc : ∀ (i : I) (hij : i ⟶ j), IsClosed (Z i hij)
hZne : ∀ (i : I) (hij : i ⟶ j), (Z i hij).Nonempty
hZcpt : ∀ (i : I) (hij : i ⟶ j), IsCompact (Z i hij)
hstab : ∀ (i i' : I) (hi'i : i' ⟶ i) (hij : i ⟶ j), Set.MapsTo (⇑(D.map hi'i)) (Z i' (hi'i ≫ hij)) (Z i hij)
this : ∀ {i₁ i₂ : Over j} (f : i₁ ⟶ i₂), IsAffineHom ((Over.forget j ⋙ D).map f)
i₁ i₂ : Over j
f : i₁ ⟶ i₂
⊢ Set.MapsTo (α := ↥((Over.forget j ⋙ D).obj i₁)) (β := ↥((Over.forget j ⋙ D).obj i₂)) (⇑((Over.forget j ⋙ D).map f))
    ((fun (i : Over j) ↦ Z i.left i.hom) i₁) ((fun (i : Over j) ↦ Z i.left i.hom) i₂)
have dsimp : Set.MapsTo (⇑(D.map (Over.Hom.left f))) (Z i₁.left i₁.hom) (Z i₂.left i₂.hom)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
j : I
Z : (i : I) → (i ⟶ j) → Set ↥(D.obj i)
hZc : ∀ (i : I) (hij : i ⟶ j), IsClosed (Z i hij)
hZne : ∀ (i : I) (hij : i ⟶ j), (Z i hij).Nonempty
hZcpt : ∀ (i : I) (hij : i ⟶ j), IsCompact (Z i hij)
hstab : ∀ (i i' : I) (hi'i : i' ⟶ i) (hij : i ⟶ j), Set.MapsTo (⇑(D.map hi'i)) (Z i' (hi'i ≫ hij)) (Z i hij)
this : ∀ {i₁ i₂ : Over j} (f : i₁ ⟶ i₂), IsAffineHom ((Over.forget j ⋙ D).map f)
i₁ i₂ : Over j
f : i₁ ⟶ i₂
⊢ Set.MapsTo (⇑(D.map (Over.Hom.left f))) (Z i₁.left i₁.hom) (Z i₂.left i₂.hom)
have rw : Set.MapsTo (⇑(D.map (Over.Hom.left f))) (Z i₁.left (Over.Hom.left f ≫ i₂.hom)) (Z i₂.left i₂.hom)
Tactic: rw [← Over.w f]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU : c.π.app i ⁻¹ᵁ U = ⊤
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = ⊤
have by_contra! : ∀ (H : ∀ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≠ ⊤), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU : c.π.app i ⁻¹ᵁ U = ⊤
H : ∀ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≠ ⊤
j : I
f : j ⟶ i
⊢ Set.Nonempty.{u} (α := ↥(D.obj j)) ((fun (j : I) (f : j ⟶ i) ↦ (↑(D.map f ⁻¹ᵁ U) : Set ↥(D.obj j))ᶜ) j f)
have simp : ¬Eq (α := Set ↥(D.obj j)) (⇑(D.map f) ⁻¹' (↑U : Set ↥(D.obj i))) Set.univ
Tactic: simp only [TopologicalSpace.Opens.map_coe, Set.nonempty_compl, ne_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU : c.π.app i ⁻¹ᵁ U = ⊤
H : ∀ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≠ ⊤
j k : I
fkj : k ⟶ j
fji : j ⟶ i
x : ↥(D.obj k)
hx : ((D.map (fkj ≫ fji)) x : ↥(D.obj i)) ∉ U
⊢ Membership.mem (α := ↥(D.obj j)) (γ := Set ↥(D.obj j))
    ((fun (j : I) (f : j ⟶ i) ↦ (↑(D.map f ⁻¹ᵁ U) : Set ↥(D.obj j))ᶜ) j fji) ((D.map fkj) x : ↥(D.obj j))
have rwa : ∀ (hx : ((D.map fkj ≫ D.map fji) x : ↥(D.obj i)) ∉ U),
  Membership.mem (α := ↥(D.obj j)) (γ := Set ↥(D.obj j))
    ((fun (j : I) (f : j ⟶ i) ↦ (↑(D.map f ⁻¹ᵁ U) : Set ↥(D.obj j))ᶜ) j fji) ((D.map fkj) x : ↥(D.obj j))
Tactic: rwa [Functor.map_comp] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU : c.π.app i ⁻¹ᵁ U = ⊤
H : ∀ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≠ ⊤
⊢ False
have obtain : ∀ (s : ↥c.pt)
  (hs :
    ∀ (i_1 : I) (hij : i_1 ⟶ i),
      Membership.mem (α := ↥(D.obj i_1)) (↑(D.map hij ⁻¹ᵁ U) : Set ↥(D.obj i_1))ᶜ ((c.π.app i_1) s : ↥(D.obj i_1))),
  False
Tactic: obtain ⟨s, hs⟩ := exists_mem_of_isClosed_of_nonempty' D c hc (fun j f ↦ (D.map f ⁻¹ᵁ U)ᶜ)
    (fun j f ↦ (D.map f ⁻¹ᵁ U).2.isClosed_compl) (fun j f ↦ by
      simp only [TopologicalSpace.Opens.map_coe, Set.nonempty_compl, ne_eq]
      exact SetLike.coe_injective.ne (H j f))
    (fun j f ↦ (D.map f ⁻¹ᵁ U).2.isClosed_compl.isCompact)
    (fun j k fkj fji x (hx : _ ∉ U) ↦ by rwa [Functor.map_comp] at hx)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
⊢ D.map j.hom ⁻¹ᵁ U ≤ D.map (Over.Hom.left f) ⁻¹ᵁ D.map k.hom ⁻¹ᵁ U
have rw : D.map j.hom ⁻¹ᵁ U ≤ (D.map (Over.Hom.left f) ≫ D.map k.hom) ⁻¹ᵁ U
Tactic: rw [← Scheme.Hom.comp_preimage, ← D.map_comp, Over.w f]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
rw : D.map j.hom ⁻¹ᵁ U ≤ (D.map (Over.Hom.left f) ≫ D.map k.hom) ⁻¹ᵁ U
⊢ D.map j.hom ⁻¹ᵁ U ≤ D.map (Over.Hom.left f) ⁻¹ᵁ D.map k.hom ⁻¹ᵁ U
have rw₁ : D.map j.hom ⁻¹ᵁ U ≤ D.map (Over.Hom.left f ≫ k.hom) ⁻¹ᵁ U
Tactic: rw [← Scheme.Hom.comp_preimage, ← D.map_comp, Over.w f]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
rw : D.map j.hom ⁻¹ᵁ U ≤ (D.map (Over.Hom.left f) ≫ D.map k.hom) ⁻¹ᵁ U
rw₁ : D.map j.hom ⁻¹ᵁ U ≤ D.map (Over.Hom.left f ≫ k.hom) ⁻¹ᵁ U
⊢ D.map j.hom ⁻¹ᵁ U ≤ D.map (Over.Hom.left f) ⁻¹ᵁ D.map k.hom ⁻¹ᵁ U
have rw₂ : D.map j.hom ⁻¹ᵁ U ≤ D.map j.hom ⁻¹ᵁ U
Tactic: rw [← Scheme.Hom.comp_preimage, ← D.map_comp, Over.w f]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
c : Cone D
hc : IsLimit c
i : I
U : (D.obj i).Opens
j : Over i
⊢ c.π.app i ⁻¹ᵁ U ≤ c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ U
have rw : c.π.app i ⁻¹ᵁ U ≤ (c.π.app j.left ≫ D.map j.hom) ⁻¹ᵁ U
Tactic: rw [← Scheme.Hom.comp_preimage, c.w]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
c : Cone D
hc : IsLimit c
i : I
U : (D.obj i).Opens
j : Over i
rw : c.π.app i ⁻¹ᵁ U ≤ (c.π.app j.left ≫ D.map j.hom) ⁻¹ᵁ U
⊢ c.π.app i ⁻¹ᵁ U ≤ c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ U
have rw₁ : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ U
Tactic: rw [← Scheme.Hom.comp_preimage, c.w]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
⊢ IsAffineHom ((opensDiagram D i U).map f)
have refine : ∀ (V : ((opensDiagram D i U).obj k).Opens) (hV : IsAffineOpen V), IsAffineOpen ((opensDiagram D i U).map f ⁻¹ᵁ V)
Tactic: refine ⟨fun V hV ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
⊢ IsAffineOpen ((opensDiagram D i U).map f ⁻¹ᵁ V)
have h : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme) →
  (opensDiagram D i U).map f ⁻¹ᵁ V = (D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V
Tactic: convert!
    ((hV.image_of_isOpenImmersion (D.map k.hom ⁻¹ᵁ U).ι).preimage
          (D.map f.left)).preimage_of_isOpenImmersion
      (D.map j.hom ⁻¹ᵁ U).ι ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
h :
  (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme) →
    (opensDiagram D i U).map f ⁻¹ᵁ V = (D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V
⊢ IsAffineOpen ((opensDiagram D i U).map f ⁻¹ᵁ V)
have this : D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V ≤ Scheme.Hom.opensRange (D.map j.hom ⁻¹ᵁ U).ι
Tactic: convert!
    ((hV.image_of_isOpenImmersion (D.map k.hom ⁻¹ᵁ U).ι).preimage
          (D.map f.left)).preimage_of_isOpenImmersion
      (D.map j.hom ⁻¹ᵁ U).ι ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
⊢ (opensDiagram D i U).map f ⁻¹ᵁ V = (D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V
have h : ∀ (x : ↥((opensDiagram D i U).obj j)),
  x ∈ (↑((opensDiagram D i U).map f ⁻¹ᵁ V) : Set ↥((opensDiagram D i U).obj j)) ↔
    x ∈
      (↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V) :
        Set ↥((opensDiagram D i U).obj j))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
⊢ x ∈ (↑((opensDiagram D i U).map f ⁻¹ᵁ V) : Set ↥((opensDiagram D i U).obj j)) ↔
    x ∈
      (↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V) :
        Set ↥((opensDiagram D i U).obj j))
have h : Membership.mem (α := ↥((opensDiagram D i U).obj k)) V (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k)) ↔
  x ∈
    (↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V) :
      Set ↥((opensDiagram D i U).obj j))
Tactic: change _ ∈ V ↔ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
⊢ Membership.mem (α := ↥((opensDiagram D i U).obj k)) V
      (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k)) ↔
    x ∈
      (↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V) :
        Set ↥((opensDiagram D i U).obj j))
have h : ∀
  (h :
    Membership.mem (α := ↥((opensDiagram D i U).obj k)) V
      (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))),
  Membership.mem (α := ↥(D.obj k.left)) (D.map k.hom ⁻¹ᵁ U)
    ((D.map (Over.Hom.left f)) (↑x : ↥(D.obj j.left)) : ↥(D.obj k.left))
Tactic: refine ⟨fun h ↦ ⟨⟨(D.map f.left).base x.1, ?_⟩, ?_, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
h :
  ∀
    (h :
      Membership.mem (α := ↥((opensDiagram D i U).obj k)) V
        (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))),
    Membership.mem (α := ↥(D.obj k.left)) (D.map k.hom ⁻¹ᵁ U)
      ((D.map (Over.Hom.left f)) (↑x : ↥(D.obj j.left)) : ↥(D.obj k.left))
⊢ Membership.mem (α := ↥((opensDiagram D i U).obj k)) V
      (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k)) ↔
    x ∈
      (↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V) :
        Set ↥((opensDiagram D i U).obj j))
have h₁ : ∀
  (h :
    Membership.mem (α := ↥((opensDiagram D i U).obj k)) V
      (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))),
  Membership.mem (α := ↥((opensDiagram D i U).obj k)) (↑V : Set ↥((opensDiagram D i U).obj k))
    (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U)
        ((D.map (Over.Hom.left f)) (↑x : ↥(D.obj j.left))) sorry :
      ↥(D.map k.hom ⁻¹ᵁ U))
Tactic: refine ⟨fun h ↦ ⟨⟨(D.map f.left).base x.1, ?_⟩, ?_, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
h :
  ∀
    (h :
      Membership.mem (α := ↥((opensDiagram D i U).obj k)) V
        (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))),
    Membership.mem (α := ↥(D.obj k.left)) (D.map k.hom ⁻¹ᵁ U)
      ((D.map (Over.Hom.left f)) (↑x : ↥(D.obj j.left)) : ↥(D.obj k.left))
h₁ :
  ∀
    (h :
      Membership.mem (α := ↥((opensDiagram D i U).obj k)) V
        (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))),
    Membership.mem (α := ↥((opensDiagram D i U).obj k)) (↑V : Set ↥((opensDiagram D i U).obj k))
      (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U)
          ((D.map (Over.Hom.left f)) (↑x : ↥(D.obj j.left))) ⋯ :
        ↥(D.map k.hom ⁻¹ᵁ U))
⊢ Membership.mem (α := ↥((opensDiagram D i U).obj k)) V
      (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k)) ↔
    x ∈
      (↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V) :
        Set ↥((opensDiagram D i U).obj j))
have h₂ : x ∈
    (↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V) :
      Set ↥((opensDiagram D i U).obj j)) →
  Membership.mem (α := ↥((opensDiagram D i U).obj k)) V (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))
Tactic: refine ⟨fun h ↦ ⟨⟨(D.map f.left).base x.1, ?_⟩, ?_, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
h :
  Membership.mem (α := ↥((opensDiagram D i U).obj k)) V (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))
⊢ Membership.mem (α := ↥(D.obj k.left)) (D.map k.hom ⁻¹ᵁ U)
    ((D.map (Over.Hom.left f)) (↑x : ↥(D.obj j.left)) : ↥(D.obj k.left))
have h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map (Over.Hom.left f) ≫ D.map k.hom) (↑x : ↥(D.obj j.left)) : ↥(D.obj i))
Tactic: change (D.map f.left ≫ D.map k.hom).base x.1 ∈ U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
h :
  Membership.mem (α := ↥((opensDiagram D i U).obj k)) V (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))
⊢ Membership.mem (α := ↥(D.obj i)) U ((D.map (Over.Hom.left f) ≫ D.map k.hom) (↑x : ↥(D.obj j.left)) : ↥(D.obj i))
have h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map j.hom) (↑x : ↥(D.obj j.left)) : ↥(D.obj i))
Tactic: rw [← D.map_comp, Over.w f]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
h :
  Membership.mem (α := ↥((opensDiagram D i U).obj k)) V (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))
⊢ Membership.mem (α := ↥((opensDiagram D i U).obj k)) (↑V : Set ↥((opensDiagram D i U).obj k))
    (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U)
        ((D.map (Over.Hom.left f)) (↑x : ↥(D.obj j.left))) ⋯ :
      ↥(D.map k.hom ⁻¹ᵁ U))
have h₁ : Eq (α := ↥((opensDiagram D i U).obj k))
  (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U)
      ((D.map (Over.Hom.left f)) (↑x : ↥(D.obj j.left))) sorry :
    ↥(D.map k.hom ⁻¹ᵁ U))
  (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))
Tactic: convert! h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV_1 : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
hU :
  Membership.mem (α := ↥(D.obj k.left)) (D.map k.hom ⁻¹ᵁ U)
    ((D.map (Over.Hom.left f)) ((D.map j.hom ⁻¹ᵁ U).ι x : ↥(D.obj j.left)) : ↥(D.obj k.left))
hV :
  Membership.mem (α := ↥((opensDiagram D i U).obj k)) (↑V : Set ↥((opensDiagram D i U).obj k))
    (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U)
        ((D.map (Over.Hom.left f)) ((D.map j.hom ⁻¹ᵁ U).ι x : ↥(D.obj j.left))) hU :
      ↥(D.map k.hom ⁻¹ᵁ U))
⊢ Membership.mem (α := ↥((opensDiagram D i U).obj k)) V (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))
have h : Eq (α := ↥((opensDiagram D i U).obj k)) (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))
  (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U)
      ((D.map (Over.Hom.left f)) ((D.map j.hom ⁻¹ᵁ U).ι x : ↥(D.obj j.left))) hU :
    ↥(D.map k.hom ⁻¹ᵁ U))
Tactic: convert! hV
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
⊢ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V ≤ Scheme.Hom.opensRange (D.map j.hom ⁻¹ᵁ U).ι
have simp : D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V ≤ D.map j.hom ⁻¹ᵁ U
Tactic: simp only [opensDiagram_obj, Scheme.Opens.opensRange_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
x : ↥(D.obj j.left)
y : ↥(D.obj k.left)
h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) y : ↥(D.obj i))
h₂ :
  Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) y h₁ ∈ (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
e :
  Eq (α := ↥(D.obj k.left))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
          (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
        (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) y h₁) :
      ↥(D.obj k.left))
    ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))
⊢ x ∈ D.map j.hom ⁻¹ᵁ U
have h₃ : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left)) : ↥(D.obj i))
Tactic: obtain rfl : y = (D.map f.left).base x := congr($e)
Cleared hypotheses: y, h₁, h₂, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
x : ↥(D.obj j.left)
y : ↥(D.obj k.left)
h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) y : ↥(D.obj i))
h₂ :
  Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) y h₁ ∈ (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
e :
  Eq (α := ↥(D.obj k.left))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
          (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
        (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) y h₁) :
      ↥(D.obj k.left))
    ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))
h₃ : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left)) : ↥(D.obj i))
⊢ x ∈ D.map j.hom ⁻¹ᵁ U
have h₄ : Membership.mem (α := ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
  (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₃ :
    ↥(D.map k.hom ⁻¹ᵁ U))
Tactic: obtain rfl : y = (D.map f.left).base x := congr($e)
Cleared hypotheses: y, h₁, h₂, e