awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
𝒰 : OpenCover.{u_1, u} X
U : X.Opens
refine_1 :
  ∀ (i : 𝒰.I₀),
    Eq (α := Set ↥(𝒰.X i)) (Set.range (ι := ↥(↑(𝒰.f i ⁻¹ᵁ U) : Scheme)) ⇑(𝒰.f i ⁻¹ᵁ U).ι)
      (Set.range (ι :=
        ↥((Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
            ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
        ⇑(pullback.snd U.ι (𝒰.f ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i))))
⊢ OpenCover.{u_1, u} (↑U : Scheme)
have refine_2 : ∀ (i : 𝒰.I₀),
  Eq (α := (↑(𝒰.f i ⁻¹ᵁ U) : Scheme) ⟶ (↑U : Scheme)) ((fun (x : 𝒰.I₀) ↦ 𝒰.f x ∣_ U) i)
    (CategoryStruct.comp (Y :=
      (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
        ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i))
      (Iso.hom
        ((fun (i : 𝒰.I₀) ↦
            (IsOpenImmersion.isoOfRangeEq (𝒰.f i ⁻¹ᵁ U).ι
                (pullback.snd U.ι
                  (𝒰.f ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
                sorry :
              (↑(𝒰.f i ⁻¹ᵁ U) : Scheme) ≅
                (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
                  ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
          i))
      ((Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).f
        ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
Tactic: refine Cover.copy (𝒰.pullback₁ U.ι) 𝒰.I₀ _ (𝒰.f · ∣_ U) (Equiv.refl _)
    (fun i ↦ IsOpenImmersion.isoOfRangeEq (Opens.ι _) (pullback.snd _ _) ?_) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
𝒰 : OpenCover.{u_1, u} X
U : X.Opens
i : 𝒰.I₀
⊢ Eq (α := Set ↥(𝒰.X i)) (Set.range (ι := ↥(↑(𝒰.f i ⁻¹ᵁ U) : Scheme)) ⇑(𝒰.f i ⁻¹ᵁ U).ι)
    (Set.range (ι :=
      ↥((Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
          ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
      ⇑(pullback.snd U.ι (𝒰.f ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i))))
have refine_1 : Eq (α := Set ↥(𝒰.X i)) (Set.range (ι := ↥(↑(𝒰.f i ⁻¹ᵁ U) : Scheme)) ⇑(𝒰.f i ⁻¹ᵁ U).ι)
  (Set.range (ι := ↥(pullback U.ι (𝒰.f i))) ⇑(pullback.snd U.ι (𝒰.f i)))
Tactic: dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
      PreZeroHypercover.pullback₁_I₀, Equiv.refl_apply, PreZeroHypercover.pullback₁_X]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
𝒰 : OpenCover.{u_1, u} X
U : X.Opens
i : 𝒰.I₀
⊢ Eq (α := Set ↥(𝒰.X i)) (Set.range (ι := ↥(↑(𝒰.f i ⁻¹ᵁ U) : Scheme)) ⇑(𝒰.f i ⁻¹ᵁ U).ι)
    (Set.range (ι := ↥(pullback U.ι (𝒰.f i))) ⇑(pullback.snd U.ι (𝒰.f i)))
have refine_1 : Set.range (ι := ↥(↑(𝒰.f i ⁻¹ᵁ U) : Scheme)) ⇑(𝒰.f i ⁻¹ᵁ U).ι = (↑(𝒰.f i ⁻¹ᵁ U) : Set ↥(𝒰.X i))
Tactic: rw [IsOpenImmersion.range_pullbackSnd U.ι (𝒰.f i), Opens.opensRange_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
𝒰 : OpenCover.{u_1, u} X
U : X.Opens
i : 𝒰.I₀
⊢ Eq (α := (↑(𝒰.f i ⁻¹ᵁ U) : Scheme) ⟶ (↑U : Scheme)) ((fun (x : 𝒰.I₀) ↦ 𝒰.f x ∣_ U) i)
    (CategoryStruct.comp (Y :=
      (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
        ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i))
      (Iso.hom
        ((fun (i : 𝒰.I₀) ↦
            (IsOpenImmersion.isoOfRangeEq (𝒰.f i ⁻¹ᵁ U).ι
                (pullback.snd U.ι
                  (𝒰.f ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
                ⋯ :
              (↑(𝒰.f i ⁻¹ᵁ U) : Scheme) ≅
                (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
                  ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
          i))
      ((Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).f
        ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
have refine_2 : Eq (α := (↑(𝒰.f i ⁻¹ᵁ U) : Scheme) ⟶ X) ((fun (x : 𝒰.I₀) ↦ 𝒰.f x ∣_ U) i ≫ U.ι)
  (CategoryStruct.comp (Y :=
      (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
        ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i))
      (Iso.hom
        ((fun (i : 𝒰.I₀) ↦
            (IsOpenImmersion.isoOfRangeEq (𝒰.f i ⁻¹ᵁ U).ι
                (pullback.snd U.ι
                  (𝒰.f ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
                sorry :
              (↑(𝒰.f i ⁻¹ᵁ U) : Scheme) ≅
                (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
                  ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
          i))
      ((Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).f
        ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)) ≫
    U.ι)
Tactic: rw [← cancel_mono U.ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
x : ↥X
hx : IsClosed (X := ↥X) {x}
⊢ height x = 0
have simp : IsMin x
Tactic: simp only [height_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
x : ↥X
hx : IsClosed (X := ↥X) {x}
b : ↥X
h : b ≤ x
⊢ x ≤ b
have inl : ∀ (hx : IsClosed (X := ↥X) {b}), b ≤ b → b ≤ b
Tactic: obtain rfl | h := eq_or_ne b x
Cleared hypotheses: x, hx, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
x : ↥X
hx : IsClosed (X := ↥X) {x}
b : ↥X
h : b ≤ x
inl : ∀ (hx : IsClosed (X := ↥X) {b}), b ≤ b → b ≤ b
⊢ x ≤ b
have inr : ∀ (h : b ≠ x), x ≤ b
Tactic: obtain rfl | h := eq_or_ne b x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (hypothesis)
Goal:
X : Scheme
x : ↥X
hx : IsClosed (X := ↥X) {x}
b : ↥X
h_1 : b ≤ x
h : b ≠ x
⊢ x ≤ b
have this : ¬x ⤳ b
Tactic: have := IsClosed.not_specializes hx rfl h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op V ⟶ op V'
⊢ appLE f U V e ≫ X.presheaf.map i = appLE f U V' ⋯
have rw : app f U ≫ X.presheaf.map ((homOfLE e).op ≫ i) = appLE f U V' sorry
Tactic: rw [Hom.appLE, Category.assoc, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op U' ⟶ op U
⊢ Y.presheaf.map i ≫ appLE f U V e = appLE f U' V ⋯
have rw : app f U' ≫ X.presheaf.map (((Opens.map f.base).map i.unop).op ≫ (homOfLE e).op) = appLE f U' V sorry
Tactic: rw [Hom.appLE, f.naturality_assoc, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₁ : U = U'
e₂ : V = V'
P : {R S : CommRingCat.{u}} → (R ⟶ S) → Prop
⊢ P (appLE f U V e) ↔ P (appLE f U' V' ⋯)
have subst : P (appLE f U V e) ↔ P (appLE f U V' sorry)
Tactic: subst e₁
Cleared hypotheses: U', e₁
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₂ : V = V'
P : {R S : CommRingCat.{u}} → (R ⟶ S) → Prop
⊢ P (appLE f U V e) ↔ P (appLE f U V' ⋯)
have subst : P (appLE f U V e) ↔ P (appLE f U V sorry)
Tactic: subst e₂
Cleared hypotheses: V', e₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f g : X ⟶ Y
h_base : f.base = g.base
h_app : ∀ (U : Y.Opens), app f U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) = app g U
⊢ f = g
have mk : ∀ (toLRSHom' : X.Hom Y.toLocallyRingedSpace) (h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = g.base)
  (h_app :
    ∀ (U : Y.Opens), { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom sorry)) = app g U),
  { toLRSHom' := toLRSHom' : X.Hom Y } = g
Tactic: cases f
Cleared hypotheses: f, h_base, h_app
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
g : X ⟶ Y
toLRSHom' : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = g.base
h_app :
  ∀ (U : Y.Opens), { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) = app g U
⊢ { toLRSHom' := toLRSHom' : X.Hom Y } = g
have mk : ∀ (toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace)
  (h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = { toLRSHom' := toLRSHom'_1 }.base)
  (h_app :
    ∀ (U : Y.Opens),
      { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom sorry)) =
        { toLRSHom' := toLRSHom'_1 : X.Hom Y }.app U),
  { toLRSHom' := toLRSHom' : X.Hom Y } = { toLRSHom' := toLRSHom'_1 }
Tactic: cases g
Cleared hypotheses: g, h_base, h_app
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
toLRSHom' toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = { toLRSHom' := toLRSHom'_1 }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
      { toLRSHom' := toLRSHom'_1 : X.Hom Y }.app U
⊢ { toLRSHom' := toLRSHom' : X.Hom Y } = { toLRSHom' := toLRSHom'_1 }
have mk : toLRSHom' = toLRSHom'_1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
toLRSHom' toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = { toLRSHom' := toLRSHom'_1 }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
      { toLRSHom' := toLRSHom'_1 : X.Hom Y }.app U
⊢ toLRSHom' = toLRSHom'_1
have mk : toLRSHom'.toHom = toLRSHom'_1.toHom
Tactic: apply LocallyRingedSpace.Hom.ext'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
toLRSHom' toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = { toLRSHom' := toLRSHom'_1 }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
      { toLRSHom' := toLRSHom'_1 : X.Hom Y }.app U
⊢ toLRSHom'.toHom = toLRSHom'_1.toHom
have mk : toLRSHom'.base = toLRSHom'_1.base
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
toLRSHom' toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = { toLRSHom' := toLRSHom'_1 }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
      { toLRSHom' := toLRSHom'_1 : X.Hom Y }.app U
mk : toLRSHom'.base = toLRSHom'_1.base
⊢ toLRSHom'.toHom = toLRSHom'_1.toHom
have mk₁ : toLRSHom'.c ≫ Functor.whiskerRight (eqToHom sorry) X.presheaf = toLRSHom'_1.c
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f g : X ⟶ Y
h : toLRSHom f = toLRSHom g
⊢ f = g
have mk : ∀ (toLRSHom' : X.Hom Y.toLocallyRingedSpace) (h : { toLRSHom' := toLRSHom' : X.Hom Y }.toLRSHom = toLRSHom g),
  { toLRSHom' := toLRSHom' : X.Hom Y } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
g : X ⟶ Y
toLRSHom' : X.Hom Y.toLocallyRingedSpace
h : { toLRSHom' := toLRSHom' : X.Hom Y }.toLRSHom = toLRSHom g
⊢ { toLRSHom' := toLRSHom' : X.Hom Y } = g
have mk : ∀ (toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace)
  (h : { toLRSHom' := toLRSHom' : X.Hom Y }.toLRSHom = { toLRSHom' := toLRSHom'_1 }.toLRSHom),
  { toLRSHom' := toLRSHom' : X.Hom Y } = { toLRSHom' := toLRSHom'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ appLE g U V e₁ ≫ appLE f V W e₂ = appLE (f ≫ g) U W ⋯
have dsimp : (app g U ≫ Y.presheaf.map (homOfLE e₁).op) ≫ app f V ≫ X.presheaf.map (homOfLE e₂).op =
  (app g U ≫ app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE sorry).op
Tactic: dsimp [Hom.appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ (app g U ≫ Y.presheaf.map (homOfLE e₁).op) ≫ app f V ≫ X.presheaf.map (homOfLE e₂).op =
    (app g U ≫ app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op
have rw : app g U ≫ app f (g ⁻¹ᵁ U) ≫ X.presheaf.map (((Opens.map f.base).map (homOfLE e₁).op.unop).op ≫ (homOfLE e₂).op) =
  (app g U ≫ app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE sorry).op
Tactic: rw [Category.assoc, f.naturality_assoc, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : X.Opens
e : V ≤ (f ≫ g) ⁻¹ᵁ U
⊢ appLE (f ≫ g) U V e = app g U ≫ appLE f (g ⁻¹ᵁ U) V e
have rw : appLE (f ≫ g) U V e = appLE g U (g ⁻¹ᵁ U) sorry ≫ appLE f (g ⁻¹ᵁ U) V e
Tactic: rw [g.app_eq_appLE, appLE_comp_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : X.Opens
e : V ≤ (f ≫ g) ⁻¹ᵁ U
rw : appLE (f ≫ g) U V e = appLE g U (g ⁻¹ᵁ U) ⋯ ≫ appLE f (g ⁻¹ᵁ U) V e
⊢ appLE (f ≫ g) U V e = app g U ≫ appLE f (g ⁻¹ᵁ U) V e
have rw₁ : appLE (f ≫ g) U V e = appLE (f ≫ g) U V sorry
Tactic: rw [g.app_eq_appLE, appLE_comp_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f g : X ⟶ Y
e : f = g
U : Y.Opens
⊢ f ⁻¹ᵁ U = g ⁻¹ᵁ U
have subst : f ⁻¹ᵁ U = f ⁻¹ᵁ U
Tactic: subst e
Cleared hypotheses: g, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f g : X ⟶ Y
e : f = g
U : Y.Opens
⊢ app f U = app g U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
have subst : app f U = app f U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom sorry))
Tactic: subst e
Cleared hypotheses: g, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
e : X = Y
U : Y.Opens
⊢ Γ(Y, U) = Γ(X, eqToHom e ⁻¹ᵁ U)
have subst : ∀ (U : X.Opens), Γ(X, U) = Γ(X, eqToHom sorry ⁻¹ᵁ U)
Tactic: subst e
Cleared hypotheses: Y, e, U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
e : X = Y
U : Y.Opens
⊢ app (eqToHom e) U = eqToHom ⋯
have subst : ∀ (U : X.Opens), app (eqToHom sorry) U = eqToHom sorry
Tactic: subst e
Cleared hypotheses: Y, e, U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : X.Opens
⊢ (f ≫ inv f) ⁻¹ᵁ U = U
have rw : 𝟙 X ⁻¹ᵁ U = U
Tactic: rw [IsIso.hom_inv_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : X.Opens
⊢ app (inv f) U = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫ inv (app f (inv f ⁻¹ᵁ U))
have rw : app (inv f) U ≫ app f (inv f ⁻¹ᵁ U) = X.presheaf.map (Quiver.Hom.op (eqToHom sorry))
Tactic: rw [IsIso.eq_comp_inv, ← comp_app, congr_app (IsIso.hom_inv_id f), id_app, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : X.Opens
rw : app (inv f) U ≫ app f (inv f ⁻¹ᵁ U) = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
⊢ app (inv f) U = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫ inv (app f (inv f ⁻¹ᵁ U))
have rw₁ : app (f ≫ inv f) U = X.presheaf.map (Quiver.Hom.op (eqToHom sorry))
Tactic: rw [IsIso.eq_comp_inv, ← comp_app, congr_app (IsIso.hom_inv_id f), id_app, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : X.Opens
rw : app (inv f) U ≫ app f (inv f ⁻¹ᵁ U) = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
rw₁ : app (f ≫ inv f) U = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
⊢ app (inv f) U = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫ inv (app f (inv f ⁻¹ᵁ U))
have rw₂ : Eq (α := Γ(X, U) ⟶ Γ(X, (f ≫ inv f) ⁻¹ᵁ U)) (app (𝟙 X) U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
  (X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
Tactic: rw [IsIso.eq_comp_inv, ← comp_app, congr_app (IsIso.hom_inv_id f), id_app, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : X.Opens
rw : app (inv f) U ≫ app f (inv f ⁻¹ᵁ U) = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
rw₁ : app (f ≫ inv f) U = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
rw₂ :
  Eq (α := Γ(X, U) ⟶ Γ(X, (f ≫ inv f) ⁻¹ᵁ U)) (app (𝟙 X) U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
    (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
⊢ app (inv f) U = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫ inv (app f (inv f ⁻¹ᵁ U))
have rw₃ : Eq (α := Γ(X, U) ⟶ Γ(X, (f ≫ inv f) ⁻¹ᵁ U)) (𝟙 Γ(X, U) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
  (X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
Tactic: rw [IsIso.eq_comp_inv, ← comp_app, congr_app (IsIso.hom_inv_id f), id_app, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : X.Opens
rw : app (inv f) U ≫ app f (inv f ⁻¹ᵁ U) = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
rw₁ : app (f ≫ inv f) U = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
rw₂ :
  Eq (α := Γ(X, U) ⟶ Γ(X, (f ≫ inv f) ⁻¹ᵁ U)) (app (𝟙 X) U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
    (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₃ :
  Eq (α := Γ(X, U) ⟶ Γ(X, (f ≫ inv f) ⁻¹ᵁ U)) (𝟙 Γ(X, U) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
    (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
⊢ app (inv f) U = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫ inv (app f (inv f ⁻¹ᵁ U))
have rw₄ : Eq (α := Γ(X, U) ⟶ Γ(X, (f ≫ inv f) ⁻¹ᵁ U)) (X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
  (X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
Tactic: rw [IsIso.eq_comp_inv, ← comp_app, congr_app (IsIso.hom_inv_id f), id_app, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X.Hom Y
g : ↥X → ↥Y
h : ⇑f = g
⊢ f.base = ofHom { toFun := g, continuous_toFun := ⋯ }
have subst : f.base = ofHom { toFun := ⇑f, continuous_toFun := sorry }
Tactic: subst h
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X.Hom Y
g : ↥X → ↥Y
h : ⇑f = g
x : ↥X
⊢ IsLocalHom (R :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                (ofHom { toFun := g, continuous_toFun := ⋯ }) :
              (a : ↥X) → ↥Y)
            x)) :
      Type u_1))
    (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
    (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  carrier) (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                  (ofHom { toFun := g, continuous_toFun := ⋯ }) :
                (a : ↥X) → ↥Y)
              x)) :
        Type u_1) →+*
      (↑(X.presheaf.stalk x) : Type u_1))
    (CommRingCat.Hom.hom
      ({ base := ofHom { toFun := g, continuous_toFun := ⋯ },
            c := f.c ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom }.stalkMap
        x))
have subst : IsLocalHom (R :=
  (↑(Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
              (ofHom { toFun := ⇑f, continuous_toFun := sorry }) :
            (a : ↥X) → ↥Y)
          x)) :
    Type u_1))
  (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
  (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                (ofHom { toFun := ⇑f, continuous_toFun := sorry }) :
              (a : ↥X) → ↥Y)
            x)) :
      Type u_1) →+*
    (↑(X.presheaf.stalk x) : Type u_1))
  (CommRingCat.Hom.hom
    ({ base := ofHom { toFun := ⇑f, continuous_toFun := sorry },
          c := f.c ≫ (Presheaf.pushforwardEq sorry X.presheaf).hom }.stalkMap
      x))
Tactic: subst h
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X.Hom Y
x : ↥X
⊢ IsLocalHom (R :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                (ofHom { toFun := ⇑f, continuous_toFun := ⋯ }) :
              (a : ↥X) → ↥Y)
            x)) :
      Type u_1))
    (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
    (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  carrier) (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                  (ofHom { toFun := ⇑f, continuous_toFun := ⋯ }) :
                (a : ↥X) → ↥Y)
              x)) :
        Type u_1) →+*
      (↑(X.presheaf.stalk x) : Type u_1))
    (CommRingCat.Hom.hom
      ({ base := ofHom { toFun := ⇑f, continuous_toFun := ⋯ },
            c := f.c ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom }.stalkMap
        x))
have h : ((↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  carrier) (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                  (ofHom
                    { toFun := ⇑f, continuous_toFun := sorry :
                      C((↑X.toPresheafedSpace.1 : Type u_1), (↑Y.toPresheafedSpace.1 : Type u_1)) }) :
                (a : ↥X) → ↥Y)
              x)) :
        Type u_1) →+*
      (↑(X.presheaf.stalk x) : Type u_1)) =
    ((↑(Y.presheaf.stalk (f x)) : Type u_1) →+* (↑(X.presheaf.stalk x) : Type u_1)) →
  Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
              (ofHom
                { toFun := ⇑f, continuous_toFun := sorry :
                  C((↑X.toPresheafedSpace.1 : Type u_1), (↑Y.toPresheafedSpace.1 : Type u_1)) }) :
            (a : ↥X) → ↥Y)
          x) =
      Y.presheaf.stalk (f x) →
    HEq (α := (↑X.toPresheafedSpace : TopCat) ⟶ (↑Y.toPresheafedSpace : TopCat))
        (ofHom { toFun := ⇑f, continuous_toFun := sorry }) (β :=
        (↑X.toPresheafedSpace : TopCat) ⟶ (↑Y.toPresheafedSpace : TopCat)) (PresheafedSpace.Hom.base f.toLRSHom'.1) →
      f.c ≫ (Presheaf.pushforwardEq sorry X.presheaf).hom = PresheafedSpace.Hom.c f.toLRSHom'.1
Tactic: convert! f.prop x using 4
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X.Hom Y
g : ↥X → ↥Y
h : ⇑f = g
⊢ f.copyBase g h = f
have subst : f.copyBase ⇑f sorry = f
Tactic: subst h
Cleared hypotheses: g, h