awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
rw :
  Eq (α := Set ↥Z)
    (Set.range (ι := ↥(pullback g f))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(pullback g f).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (pullback.fst g f))) ≫
              g.base)) :
        (a : ↥(pullback g f)) → ↥Z))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₁ :
  Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback g f)) (Function.comp (β := ↥Y) ⇑g ⇑(pullback.fst g f)))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₂ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥(pullback g f)) ⇑(pullback.fst g f)))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₃ :
  Eq (α := Set ↥Z) (⇑g '' (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)) (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₄ :
  Eq (α := Set ↥Z) (⇑g '' (↑{ carrier := ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ : Opens ↥Y } : Set ↥Y))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₅ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₆ : (Scheme.Hom.opensRange f).carrier ∩ Set.range (ι := ↥Y) ⇑g = Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback g f)) ⇑(pullback.fst g f ≫ g))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
have rw₇ : Set.range (ι := ↥Y) ⇑g ∩ (Scheme.Hom.opensRange f).carrier = Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f
Tactic: rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, range_pullbackFst,
    Opens.map_obj, Opens.coe_mk, Set.image_preimage_eq_inter_range,
    Set.inter_comm, Opens.carrier_eq_coe, Scheme.Hom.coe_opensRange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
rw :
  Eq (α := Set ↥Z)
    (Set.range (ι := ↥(pullback g f))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(pullback g f).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (pullback.fst g f))) ≫
              g.base)) :
        (a : ↥(pullback g f)) → ↥Z))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₁ :
  Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback g f)) (Function.comp (β := ↥Y) ⇑g ⇑(pullback.fst g f)))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₂ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥(pullback g f)) ⇑(pullback.fst g f)))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₃ :
  Eq (α := Set ↥Z) (⇑g '' (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)) (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₄ :
  Eq (α := Set ↥Z) (⇑g '' (↑{ carrier := ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ : Opens ↥Y } : Set ↥Y))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₅ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₆ : (Scheme.Hom.opensRange f).carrier ∩ Set.range (ι := ↥Y) ⇑g = Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f
rw₇ : Set.range (ι := ↥Y) ⇑g ∩ (Scheme.Hom.opensRange f).carrier = Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback g f)) ⇑(pullback.fst g f ≫ g))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
have rw₈ : Set.range (ι := ↥Y) ⇑g ∩ (↑(Scheme.Hom.opensRange f) : Set ↥Z) = Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f
Tactic: rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, range_pullbackFst,
    Opens.map_obj, Opens.coe_mk, Set.image_preimage_eq_inter_range,
    Set.inter_comm, Opens.carrier_eq_coe, Scheme.Hom.coe_opensRange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
rw :
  Eq (α := Set ↥Z)
    (Set.range (ι := ↥(pullback g f))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(pullback g f).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (pullback.fst g f))) ≫
              g.base)) :
        (a : ↥(pullback g f)) → ↥Z))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₁ :
  Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback g f)) (Function.comp (β := ↥Y) ⇑g ⇑(pullback.fst g f)))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₂ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥(pullback g f)) ⇑(pullback.fst g f)))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₃ :
  Eq (α := Set ↥Z) (⇑g '' (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)) (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₄ :
  Eq (α := Set ↥Z) (⇑g '' (↑{ carrier := ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ : Opens ↥Y } : Set ↥Y))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₅ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₆ : (Scheme.Hom.opensRange f).carrier ∩ Set.range (ι := ↥Y) ⇑g = Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f
rw₇ : Set.range (ι := ↥Y) ⇑g ∩ (Scheme.Hom.opensRange f).carrier = Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f
rw₈ : Set.range (ι := ↥Y) ⇑g ∩ (↑(Scheme.Hom.opensRange f) : Set ↥Z) = Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback g f)) ⇑(pullback.fst g f ≫ g))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
have rw₉ : Eq (α := Set ↥Z) (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
Tactic: rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, range_pullbackFst,
    Opens.map_obj, Opens.coe_mk, Set.image_preimage_eq_inter_range,
    Set.inter_comm, Opens.carrier_eq_coe, Scheme.Hom.coe_opensRange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
⊢ iU ''ᵁ f' ⁻¹ᵁ W = f ⁻¹ᵁ iV ''ᵁ W
have h : ∀ (x : ↥X), x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
⊢ x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)
have pos : ∀ (hx : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥U) ⇑iU) x),
  x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)
Tactic: by_cases hx : x ∈ Set.range iU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
pos :
  ∀ (hx : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥U) ⇑iU) x),
    x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)
⊢ x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)
have neg : ∀ (hx : x ∉ Set.range (ι := ↥U) ⇑iU), x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)
Tactic: by_cases hx : x ∈ Set.range iU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
hx : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥U) ⇑iU) x
⊢ x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)
have pos : ∀ (x : ↥U),
  Membership.mem (α := ↥X) (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) (iU x : ↥X) ↔
    Membership.mem (α := ↥X) (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X) (iU x : ↥X)
Tactic: obtain ⟨x, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥U
⊢ Membership.mem (α := ↥X) (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) (iU x : ↥X) ↔
    Membership.mem (α := ↥X) (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X) (iU x : ↥X)
have pos : Membership.mem (α := ↥X) (iU ''ᵁ f' ⁻¹ᵁ W) (iU x : ↥X) ↔ Membership.mem (α := ↥Y) (iV ''ᵁ W) ((f' ≫ iV) x : ↥Y)
Tactic: simp only [SetLike.mem_coe, Opens.map_coe, Set.mem_preimage, ← Scheme.Hom.comp_apply, ← H.w]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
hx : x ∉ Set.range (ι := ↥U) ⇑iU
⊢ x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)
have neg : x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) → x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
hx : x ∉ Set.range (ι := ↥U) ⇑iU
neg : x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) → x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)
⊢ x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)
have neg₁ : x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X) → x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
hx : x ∉ Set.range (ι := ↥U) ⇑iU
y : ↥V
hy : y ∈ (↑W : Set ↥V)
e : Eq (α := ↥Y) (iV y : ↥Y) (f x : ↥Y)
⊢ x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X)
have neg : ∀ (x : ↥(pullback iV f)) (hx : ((pullback.snd iV f) x : ↥X) ∉ Set.range (ι := ↥U) ⇑iU)
  (e : Eq (α := ↥Y) (iV y : ↥Y) (f ((pullback.snd iV f) x : ↥X) : ↥Y)),
  Membership.mem (α := ↥X) (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ((pullback.snd iV f) x : ↥X)
Tactic: obtain ⟨x, rfl⟩ := (IsOpenImmersion.range_pullbackSnd iV f).ge ⟨y, e⟩
Cleared hypotheses: x, hx, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (hypothesis)
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
y : ↥V
hy : y ∈ (↑W : Set ↥V)
x : ↥(pullback iV f)
hx : ((pullback.snd iV f) x : ↥X) ∉ Set.range (ι := ↥U) ⇑iU
e : Eq (α := ↥Y) (iV y : ↥Y) (f ((pullback.snd iV f) x : ↥X) : ↥Y)
⊢ Membership.mem (α := ↥X) (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ((pullback.snd iV f) x : ↥X)
have hx₁ : ((Iso.inv H.isoPullback ≫ iU) x : ↥X) ∉ Set.range (ι := ↥U) ⇑iU
Tactic: rw [← H.isoPullback_inv_snd] at hx
Cleared hypotheses: hx, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst : IsOpenImmersion g
H : Subset (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥U) ⇑g)
⊢ IsPullback (lift g f H) (𝟙 X) g f
have h : lift g f H = lift g f H ≫ 𝟙 U
Tactic: convert! IsPullback.of_id_snd.paste_horiz (IsKernelPair.id_of_mono g)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst : IsOpenImmersion g
H : Subset (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥U) ⇑g)
h : lift g f H = lift g f H ≫ 𝟙 U
⊢ IsPullback (lift g f H) (𝟙 X) g f
have h₁ : f = lift g f H ≫ g
Tactic: convert! IsPullback.of_id_snd.paste_horiz (IsKernelPair.id_of_mono g)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst : IsOpenImmersion g
H : Subset (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥U) ⇑g)
h : lift g f H = lift g f H ≫ 𝟙 U
h₁ : f = lift g f H ≫ g
⊢ IsPullback (lift g f H) (𝟙 X) g f
have convert_2 : X ⟶ U
Tactic: convert! IsPullback.of_id_snd.paste_horiz (IsKernelPair.id_of_mono g)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst_1 : IsOpenImmersion g
e : Eq (α := Set ↥Z) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)
⊢ lift g f ⋯ ≫ lift f g ⋯ = 𝟙 X
have rw : (lift g f sorry ≫ lift f g sorry) ≫ f = 𝟙 X ≫ f
Tactic: rw [← cancel_mono f]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst_1 : IsOpenImmersion g
e : Eq (α := Set ↥Z) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)
⊢ lift f g ⋯ ≫ lift g f ⋯ = 𝟙 Y
have rw : (lift f g sorry ≫ lift g f sorry) ≫ g = 𝟙 Y ≫ g
Tactic: rw [← cancel_mono g]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
fg : Y ⟶ X
H : fg = f ≫ g
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app fg (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have subst : Scheme.Hom.app f V =
  CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
    (Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
Tactic: subst H
Cleared hypotheses: fg, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have rw : Scheme.Hom.app f V =
  CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
    ((Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V)) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
Tactic: rw [Scheme.Hom.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc,
    ← Functor.map_comp, ← op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans,
    eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
rw :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      ((Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V)) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
⊢ Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have rw₁ : Scheme.Hom.app f V =
  CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
    (Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
Tactic: rw [Scheme.Hom.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc,
    ← Functor.map_comp, ← op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans,
    eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
rw :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      ((Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V)) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₁ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
⊢ Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have rw₂ : Scheme.Hom.app f V =
  CategoryStruct.comp (Y := Γ(U, g ⁻¹ᵁ g ''ᵁ V)) (U.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
    (Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
Tactic: rw [Scheme.Hom.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc,
    ← Functor.map_comp, ← op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans,
    eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
rw :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      ((Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V)) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₁ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₂ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(U, g ⁻¹ᵁ g ''ᵁ V)) (U.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
      (Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
⊢ Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have rw₃ : Scheme.Hom.app f V =
  Scheme.Hom.app f V ≫
    CategoryStruct.comp (Y := Γ(Y, f ⁻¹ᵁ g ⁻¹ᵁ g ''ᵁ V))
      (Y.presheaf.map (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom sorry))))))
      (Y.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
Tactic: rw [Scheme.Hom.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc,
    ← Functor.map_comp, ← op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans,
    eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
rw :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      ((Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V)) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₁ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₂ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(U, g ⁻¹ᵁ g ''ᵁ V)) (U.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
      (Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₃ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      CategoryStruct.comp (Y := Γ(Y, f ⁻¹ᵁ g ⁻¹ᵁ g ''ᵁ V))
        (Y.presheaf.map (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))))
        (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
⊢ Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have rw₄ : Scheme.Hom.app f V =
  Scheme.Hom.app f V ≫
    Y.presheaf.map
      (CategoryStruct.comp (Y := op ((Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)))
        (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom sorry)))))
        (Quiver.Hom.op (eqToHom sorry)))
Tactic: rw [Scheme.Hom.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc,
    ← Functor.map_comp, ← op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans,
    eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
rw :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      ((Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V)) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₁ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₂ :
  Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(U, g ⁻¹ᵁ g ''ᵁ V)) (U.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
      (Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₃ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      CategoryStruct.comp (Y := Γ(Y, f ⁻¹ᵁ g ⁻¹ᵁ g ''ᵁ V))
        (Y.presheaf.map (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯))))))
        (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₄ :
  Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫
      Y.presheaf.map
        (CategoryStruct.comp (Y := op ((Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)))
          (Quiver.Hom.op ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯)))))
          (Quiver.Hom.op (eqToHom ⋯)))
⊢ Scheme.Hom.app f V =
    CategoryStruct.comp (Y := Γ(X, g ''ᵁ V)) (Iso.inv (Scheme.Hom.appIso g V))
      (Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have rw₅ : Scheme.Hom.app f V =
  Scheme.Hom.app f V ≫
    Y.presheaf.map
      (CategoryStruct.comp (Y := (Opens.map f.base).obj (g ⁻¹ᵁ g ''ᵁ V)) (eqToHom sorry : f ⁻¹ᵁ V ⟶ (f ≫ g) ⁻¹ᵁ g ''ᵁ V)
          ((Opens.map f.base).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom sorry))))).op
Tactic: rw [Scheme.Hom.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc,
    ← Functor.map_comp, ← op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans,
    eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id]