awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (hypothesis)
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
e₁ :
  Eq (α := Γ(X, V.ι ''ᵁ W) ⟶ Γ((↑U : Scheme), (X.homOfLE e ≫ V.ι) ⁻¹ᵁ V.ι ''ᵁ W))
    (Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W))
    (Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V : Scheme).presheaf.map (Quiver.Hom.op (Iso.hom (eqToIso this))) ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫
      (↑U : Scheme).presheaf.map
        ((Opens.map (X.homOfLE e).base).map (Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (eqToIso this))))).op
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op
have e₃ : Hom.app (X.homOfLE e) W ≫
    (↑U : Scheme).presheaf.map
      ((Opens.map (X.homOfLE e).base).map (Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (eqToIso this))))).op =
  Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom sorry))
Tactic: have e₃ := e₂.symm.trans e₁
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (hypothesis)
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
e₁ :
  Eq (α := Γ(X, V.ι ''ᵁ W) ⟶ Γ((↑U : Scheme), (X.homOfLE e ≫ V.ι) ⁻¹ᵁ V.ι ''ᵁ W))
    (Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W))
    (Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V : Scheme).presheaf.map (Quiver.Hom.op (Iso.hom (eqToIso this))) ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫
      (↑U : Scheme).presheaf.map
        ((Opens.map (X.homOfLE e).base).map (Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (eqToIso this))))).op
e₃ :
  Hom.app (X.homOfLE e) W ≫
      X.presheaf.map ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op =
    CategoryStruct.comp (Y := Γ((↑U : Scheme), U.ι ⁻¹ᵁ V.ι ''ᵁ W)) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (X.presheaf.map (Quiver.Hom.op ((Hom.opensFunctor U.ι).map (eqToHom ⋯))))
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op
have e₄ : Hom.app (X.homOfLE e) W =
  X.presheaf.map
      (CategoryStruct.comp (Y := op (U.ι ''ᵁ U.ι ⁻¹ᵁ V.ι ''ᵁ W)) (Quiver.Hom.op (homOfLE sorry))
        (Quiver.Hom.op ((Hom.opensFunctor U.ι).map (eqToHom sorry)))) ≫
    X.presheaf.map (inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op)
Tactic: rw [← IsIso.eq_comp_inv, ← Functor.map_inv, ← Functor.map_comp] at e₃
Cleared hypotheses: e₃
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
e₁ :
  Eq (α := Γ(X, V.ι ''ᵁ W) ⟶ Γ((↑U : Scheme), (X.homOfLE e ≫ V.ι) ⁻¹ᵁ V.ι ''ᵁ W))
    (Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W))
    (Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V : Scheme).presheaf.map (Quiver.Hom.op (Iso.hom (eqToIso this))) ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫
      (↑U : Scheme).presheaf.map
        ((Opens.map (X.homOfLE e).base).map (Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (eqToIso this))))).op
e₃ :
  Hom.app (X.homOfLE e) W =
    X.presheaf.map
        (CategoryStruct.comp (Y := op (U.ι ''ᵁ U.ι ⁻¹ᵁ V.ι ''ᵁ W)) (Quiver.Hom.op (homOfLE ⋯))
          (Quiver.Hom.op ((Hom.opensFunctor U.ι).map (eqToHom ⋯)))) ≫
      X.presheaf.map (inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op)
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op
have rw : X.presheaf.map
    (CategoryStruct.comp (Y := op (U.ι ''ᵁ U.ι ⁻¹ᵁ V.ι ''ᵁ W)) (Quiver.Hom.op (homOfLE sorry))
        (Quiver.Hom.op ((Hom.opensFunctor U.ι).map (eqToHom sorry))) ≫
      inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op) =
  X.presheaf.map (homOfLE sorry).op
Tactic: rw [e₃, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
⊢ Membership.mem (γ := Set (Presieve (↑(⨆ (i : J), U i) : Scheme)))
    ((precoverage IsOpenImmersion).coverings (↑(⨆ (i : J), U i) : Scheme))
    (PreZeroHypercover.presieve₀.{u_1, u_2, u_2 + 1}
      { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ })
have rw : (∀ (x : ↥(↑(⨆ (i : J), U i) : Scheme)),
    ∃ (i :
      PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
        { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE sorry }),
      Membership.mem (γ := Set ↥(↑(⨆ (i : J), U i) : Scheme))
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE sorry :
                PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE sorry :
                PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
              i))
        x) ∧
  ∀
    (i :
      PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
        { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE sorry }),
    IsOpenImmersion
      (PreZeroHypercover.f
        { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE sorry :
          PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
        i)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
⊢ (∀ (x : ↥(↑(⨆ (i : J), U i) : Scheme)),
      ∃ (i :
        PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
          { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ }),
        Membership.mem (γ := Set ↥(↑(⨆ (i : J), U i) : Scheme))
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
                  PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
                  PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
          { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
            PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
          i)
have refine : ∀ (x : ↥(↑(⨆ (i : J), U i) : Scheme)),
  ∃ (i :
    PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
      { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE sorry }),
    Membership.mem (γ := Set ↥(↑(⨆ (i : J), U i) : Scheme))
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE sorry :
              PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE sorry :
              PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
            i))
      x
Tactic: refine ⟨fun x ↦ ?_, inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
x : ↥(↑(⨆ (i : J), U i) : Scheme)
⊢ ∃ (i :
    PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
      { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ }),
    Membership.mem (γ := Set ↥(↑(⨆ (i : J), U i) : Scheme))
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
              PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
              PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
            i))
      x
have obtain : ∀ (i : J) (hi : (↑x : ↥X) ∈ U i),
  ∃ (i :
    PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
      { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE sorry }),
    Membership.mem (γ := Set ↥(↑(⨆ (i : J), U i) : Scheme))
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE sorry :
              PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE sorry :
              PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
            i))
      x
Tactic: obtain ⟨i, hi⟩ := TopologicalSpace.Opens.mem_iSup.mp x.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
x : ↥(↑(⨆ (i : J), U i) : Scheme)
i : J
hi : (↑x : ↥X) ∈ U i
⊢ ∃ (i :
    PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
      { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ }),
    Membership.mem (γ := Set ↥(↑(⨆ (i : J), U i) : Scheme))
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
              PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
              PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
            i))
      x
have h : (PreZeroHypercover.f { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE sorry } i)
    (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U i) (↑x : ↥X) hi) =
  x
Tactic: use i, ⟨x.1, hi⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
x : ↥(↑(⨆ (i : J), U i) : Scheme)
i : J
hi : (↑x : ↥X) ∈ U i
⊢ (PreZeroHypercover.f { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ } i)
      (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U i) (↑x : ↥X) hi) =
    x
have h : (↑((PreZeroHypercover.f { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE sorry } i)
        (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U i) (↑x : ↥X) hi)) :
    ↥X) =
  (↑x : ↥X)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U_1 U : X.Opens
⊢ Over.homMk (X.homOfLE ⋯) ⋯ = 𝟙 (Over.mk U.ι)
have h : Over.Hom.left (Over.homMk (X.homOfLE sorry) sorry) = Over.Hom.left (𝟙 (Over.mk U.ι))
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U_1 U V W : X.Opens
i : U ⟶ V
j : V ⟶ W
⊢ Eq.{u + 1} (α := Over.mk U.ι ⟶ Over.mk W.ι) (Over.homMk (X.homOfLE ⋯) ⋯)
    (CategoryStruct.comp (Y := Over.mk V.ι) (Over.homMk (X.homOfLE ⋯) ⋯) (Over.homMk (X.homOfLE ⋯) ⋯))
have h : Eq.{u + 1} (α := (Over.mk U.ι).left ⟶ (Over.mk W.ι).left) (Over.Hom.left (Over.homMk (X.homOfLE sorry) sorry))
  (Over.Hom.left (CategoryStruct.comp (Y := Over.mk V.ι) (Over.homMk (X.homOfLE sorry) sorry) (Over.homMk (X.homOfLE sorry) sorry)))
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U_1 : X.Opens
U V : X.Opensᵒᵖ
i : U ⟶ V
⊢ (X.restrictFunctor.op ⋙ Functor.op (Over.forget X) ⋙ Γ).map i ≫
      Iso.hom ((fun (U : X.Opensᵒᵖ) ↦ Functor.mapIso X.presheaf (Iso.op (Iso.symm (eqToIso ⋯)))) V) =
    Iso.hom ((fun (U : X.Opensᵒᵖ) ↦ Functor.mapIso X.presheaf (Iso.op (Iso.symm (eqToIso ⋯)))) U) ≫ X.presheaf.map i
have dsimp : Hom.appTop (X.homOfLE sorry) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom sorry)) =
  X.presheaf.map (Quiver.Hom.op (eqToHom sorry)) ≫ X.presheaf.map i
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U_1 : X.Opens
U V : X.Opensᵒᵖ
i : U ⟶ V
⊢ Hom.appTop (X.homOfLE ⋯) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
    X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫ X.presheaf.map i
have rw : X.presheaf.map (Quiver.Hom.op (homOfLE sorry) ≫ Quiver.Hom.op (eqToHom sorry)) = X.presheaf.map (Quiver.Hom.op (eqToHom sorry) ≫ i)
Tactic: rw [X.homOfLE_appTop, ← Functor.map_comp, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
X : Scheme
U V : X.Opens
e : U = V
⊢ Eq (α := Set ↥X) (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι) (Set.range (ι := ↥(↑V : Scheme)) ⇑V.ι)
have rw : Eq (α := Set ↥X) (Set.range (ι := ↥(↑V : Scheme)) ⇑V.ι) (Set.range (ι := ↥(↑V : Scheme)) ⇑V.ι)
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
⊢ X.isoOfEq ⋯ = Iso.refl (↑U : Scheme)
have w : (X.isoOfEq sorry).hom = Iso.hom (Iso.refl (↑U : Scheme))
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
⊢ (X.isoOfEq ⋯).hom = Iso.hom (Iso.refl (↑U : Scheme))
have w : (X.isoOfEq sorry).hom ≫ U.ι = Iso.hom (Iso.refl (↑U : Scheme)) ≫ U.ι
Tactic: rw [← cancel_mono U.ι, Scheme.isoOfEq_hom_ι, Iso.refl_hom, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
w : (X.isoOfEq ⋯).hom ≫ U.ι = Iso.hom (Iso.refl (↑U : Scheme)) ≫ U.ι
⊢ (X.isoOfEq ⋯).hom = Iso.hom (Iso.refl (↑U : Scheme))
have w₁ : U.ι = Iso.hom (Iso.refl (↑U : Scheme)) ≫ U.ι
Tactic: rw [← cancel_mono U.ι, Scheme.isoOfEq_hom_ι, Iso.refl_hom, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
w : (X.isoOfEq ⋯).hom ≫ U.ι = Iso.hom (Iso.refl (↑U : Scheme)) ≫ U.ι
w₁ : U.ι = Iso.hom (Iso.refl (↑U : Scheme)) ≫ U.ι
⊢ (X.isoOfEq ⋯).hom = Iso.hom (Iso.refl (↑U : Scheme))
have w₂ : U.ι = 𝟙 (↑U : Scheme) ≫ U.ι
Tactic: rw [← cancel_mono U.ι, Scheme.isoOfEq_hom_ι, Iso.refl_hom, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
w : (X.isoOfEq ⋯).hom ≫ U.ι = Iso.hom (Iso.refl (↑U : Scheme)) ≫ U.ι
w₁ : U.ι = Iso.hom (Iso.refl (↑U : Scheme)) ≫ U.ι
w₂ : U.ι = 𝟙 (↑U : Scheme) ≫ U.ι
⊢ (X.isoOfEq ⋯).hom = Iso.hom (Iso.refl (↑U : Scheme))
have w₃ : U.ι = U.ι
Tactic: rw [← cancel_mono U.ι, Scheme.isoOfEq_hom_ι, Iso.refl_hom, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst_1 : IsIso f
U : Y.Opens
⊢ (↑(f ⁻¹ᵁ U) : Scheme) ≅ (↑U : Scheme)
have apply : Eq (α := Set ↥Y) (Set.range (ι := ↥(↑(f ⁻¹ᵁ U) : Scheme)) ⇑((f ⁻¹ᵁ U).ι ≫ f)) (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)
Tactic: apply IsOpenImmersion.isoOfRangeEq (f := (f ⁻¹ᵁ U).ι ≫ f) U.ι _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst_1 : IsIso f
U : Y.Opens
⊢ Eq (α := Set ↥Y) (Set.range (ι := ↥(↑(f ⁻¹ᵁ U) : Scheme)) ⇑((f ⁻¹ᵁ U).ι ≫ f)) (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)
have dsimp : Eq (α := Set ↥Y)
  (Set.range (ι := ↥(↑(f ⁻¹ᵁ U) : Scheme))
    (Function.comp (β := ↥X) (⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥Y)
      (⇑(TopCat.Hom.hom (f ⁻¹ᵁ U).ι.base) : (a : ↥(↑(f ⁻¹ᵁ U) : Scheme)) → ↥X)))
  (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst_1 : IsIso f
U : Y.Opens
⊢ Eq (α := Set ↥Y)
    (Set.range (ι := ↥(↑(f ⁻¹ᵁ U) : Scheme))
      (Function.comp (β := ↥X) (⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥Y)
        (⇑(TopCat.Hom.hom (f ⁻¹ᵁ U).ι.base) : (a : ↥(↑(f ⁻¹ᵁ U) : Scheme)) → ↥X)))
    (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)
have rw : (⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥Y) '' (↑(f ⁻¹ᵁ U) : Set ↥X) = (↑U : Set ↥Y)
Tactic: rw [Set.range_comp, Opens.range_ι, Opens.range_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (hypothesis)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
⊢ Eq (α := Set ↥X) (Set.range (ι := ↥(↑(V.ι ⁻¹ᵁ U) : Scheme)) ⇑((V.ι ⁻¹ᵁ U).ι ≫ V.ι))
    (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)
have this : V.ι ''ᵁ V.ι ⁻¹ᵁ U = U
Tactic: have : V.ι ''ᵁ (V.ι ⁻¹ᵁ U) = U := by simpa [Scheme.Hom.image_preimage_eq_opensRange_inf]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
this : V.ι ''ᵁ V.ι ⁻¹ᵁ U = U
⊢ Eq (α := Set ↥X) (Set.range (ι := ↥(↑(V.ι ⁻¹ᵁ U) : Scheme)) ⇑((V.ι ⁻¹ᵁ U).ι ≫ V.ι))
    (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)
have rw : Set.image (α := ↥(↑V : Scheme)) (⇑V.ι)
    (Set.range (ι := ↥(↑(V.ι ⁻¹ᵁ V.ι ''ᵁ V.ι ⁻¹ᵁ U) : Scheme)) ⇑(V.ι ⁻¹ᵁ V.ι ''ᵁ V.ι ⁻¹ᵁ U).ι) =
  (↑(V.ι ''ᵁ V.ι ⁻¹ᵁ U) : Set ↥X)
Tactic: rw [Scheme.Hom.comp_base, TopCat.coe_comp, Scheme.Opens.range_ι, Set.range_comp, ← this]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
R : CommRingCat
f : (↑R : Type u)
⊢ Eq (α := Set ↥(Spec R))
    (Set.range (ι := ↥(↑(PrimeSpectrum.basicOpen f) : Scheme)) ⇑(Scheme.Opens.ι (PrimeSpectrum.basicOpen f)))
    (Set.range (ι := ↥(Spec (CommRingCat.of (Localization.Away f))))
      ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f)))))
have simp : (↑(PrimeSpectrum.basicOpen f) : Set ↥(Spec R)) =
  Set.range (ι := ↥(Spec (CommRingCat.of (Localization.Away f))))
    ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f))))
Tactic: simp only [Scheme.Opens.range_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
R : CommRingCat
f g x : (↑R : Type u)
hx : x = f * g
⊢ IsLocalization.Away (f * g) (Localization.Away x)
have rw : IsLocalization.Away (f * g) (Localization.Away (f * g))
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
R : CommRingCat
f g x : (↑R : Type u)
hx : x = f * g
⊢ (basicOpenIsoSpecAway x).inv ≫ (Spec R).homOfLE ⋯ =
    Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv
have subst : (basicOpenIsoSpecAway (f * g)).inv ≫ (Spec R).homOfLE sorry =
  Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv
Tactic: subst hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
R : CommRingCat
f g : (↑R : Type u)
⊢ (basicOpenIsoSpecAway (f * g)).inv ≫ (Spec R).homOfLE ⋯ =
    Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv
have rw : ((basicOpenIsoSpecAway (f * g)).inv ≫ (Spec R).homOfLE sorry) ≫ Scheme.Opens.ι (PrimeSpectrum.basicOpen f) =
  (Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv) ≫
    Scheme.Opens.ι (PrimeSpectrum.basicOpen f)
Tactic: rw [← cancel_mono (Scheme.Opens.ι _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
R : CommRingCat
f g : (↑R : Type u)
⊢ ((basicOpenIsoSpecAway (f * g)).inv ≫ (Spec R).homOfLE ⋯) ≫ Scheme.Opens.ι (PrimeSpectrum.basicOpen f) =
    (Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv) ≫
      Scheme.Opens.ι (PrimeSpectrum.basicOpen f)
have simp : Eq (α := Spec (CommRingCat.of (Localization.Away (f * g))) ⟶ Spec R)
  (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away (f * g)))))
  (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away f)))
    (Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f)))))
Tactic: simp only [basicOpenIsoSpecAway, Category.assoc, Scheme.homOfLE_ι,
    IsOpenImmersion.isoOfRangeEq_inv_fac]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
R : CommRingCat
f g : (↑R : Type u)
⊢ Eq (α := Spec (CommRingCat.of (Localization.Away (f * g))) ⟶ Spec R)
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away (f * g)))))
    (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away f)))
      (Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f)))))
have simp : Eq (α := Spec (CommRingCat.of (Localization.Away (f * g))) ⟶ Spec R)
  (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away (f * g)))))
  (Spec.map
    (CommRingCat.ofHom
      (@RingHom.comp _ (Localization.Away f) _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.awayToAwayRight f g)
        (algebraMap (↑R : Type u) (Localization.Away f)))))
Tactic: simp only [← Spec.map_comp, ← CommRingCat.ofHom_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
R : CommRingCat
f g : (↑R : Type u)
⊢ Eq (α := Spec (CommRingCat.of (Localization.Away (f * g))) ⟶ Spec R)
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away (f * g)))))
    (Spec.map
      (CommRingCat.ofHom
        (@RingHom.comp _ (Localization.Away f) _ _ Semiring.toNonAssocSemiring _
          (IsLocalization.Away.awayToAwayRight f g) (algebraMap (↑R : Type u) (Localization.Away f)))))
have e_f : Eq (α := (↑R : Type u) →+* Localization.Away (f * g)) (algebraMap (↑R : Type u) (Localization.Away (f * g)))
  (@RingHom.comp _ (Localization.Away f) _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.awayToAwayRight f g)
    (algebraMap (↑R : Type u) (Localization.Away f)))
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
R : CommRingCat
f g : (↑R : Type u)
⊢ Eq (α := (↑R : Type u) →+* Localization.Away (f * g)) (algebraMap (↑R : Type u) (Localization.Away (f * g)))
    (@RingHom.comp _ (Localization.Away f) _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.awayToAwayRight f g)
      (algebraMap (↑R : Type u) (Localization.Away f)))
have e_f : ∀ (x : (↑R : Type u)),
  Eq (α := Localization.Away (f * g))
    ((algebraMap (↑R : Type u) (Localization.Away (f * g)) : (a : (↑R : Type u)) → Localization.Away (f * g)) x :
      Localization.Away (f * g))
    ((@RingHom.comp _ (Localization.Away f) _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.awayToAwayRight f g)
            (algebraMap (↑R : Type u) (Localization.Away f)) :
          (a : (↑R : Type u)) → Localization.Away (f * g))
        x :
      Localization.Away (f * g))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ pullback f U.ι ≅ (↑(f ⁻¹ᵁ U) : Scheme)
have refine : Eq (α := Set ↥X) (Set.range (ι := ↥(pullback f U.ι)) ⇑(pullback.fst f U.ι))
  (Set.range (ι := ↥(↑(f ⁻¹ᵁ U) : Scheme)) ⇑(f ⁻¹ᵁ U).ι)
Tactic: refine IsOpenImmersion.isoOfRangeEq (pullback.fst f _) (Scheme.Opens.ι _) ?_