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 f g)) ⇑(pullback.snd f g ≫ g))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₁ :
  Eq (α := Set ↥Z)
    (Set.range (ι := ↥(pullback f g))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(pullback f g).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (pullback.snd f g))) ≫
              g.base)) :
        (a : ↥(pullback f g)) → ↥Z))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₂ :
  Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) (Function.comp (β := ↥Y) ⇑g ⇑(pullback.snd f g)))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g ≫ f))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
have rw₃ : Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)))
  (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
Tactic: rw [pullback.condition, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
    range_pullbackSnd, Opens.map_obj, Opens.coe_mk,
    Set.image_preimage_eq_inter_range, 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 f g)) ⇑(pullback.snd f g ≫ g))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₁ :
  Eq (α := Set ↥Z)
    (Set.range (ι := ↥(pullback f g))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(pullback f g).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (pullback.snd f g))) ≫
              g.base)) :
        (a : ↥(pullback f g)) → ↥Z))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₂ :
  Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) (Function.comp (β := ↥Y) ⇑g ⇑(pullback.snd f g)))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₃ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g ≫ f))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
have rw₄ : Eq (α := Set ↥Z) (⇑g '' (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)) (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
Tactic: rw [pullback.condition, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
    range_pullbackSnd, Opens.map_obj, Opens.coe_mk,
    Set.image_preimage_eq_inter_range, 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 f g)) ⇑(pullback.snd f g ≫ g))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₁ :
  Eq (α := Set ↥Z)
    (Set.range (ι := ↥(pullback f g))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(pullback f g).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (pullback.snd f g))) ≫
              g.base)) :
        (a : ↥(pullback f g)) → ↥Z))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₂ :
  Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) (Function.comp (β := ↥Y) ⇑g ⇑(pullback.snd f g)))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₃ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₄ :
  Eq (α := Set ↥Z) (⇑g '' (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)) (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g ≫ f))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
have rw₅ : Eq (α := Set ↥Z) (⇑g '' (↑{ carrier := ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier, is_open' := sorry : Opens ↥Y } : Set ↥Y))
  (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
Tactic: rw [pullback.condition, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
    range_pullbackSnd, Opens.map_obj, Opens.coe_mk,
    Set.image_preimage_eq_inter_range, 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 f g)) ⇑(pullback.snd f g ≫ g))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₁ :
  Eq (α := Set ↥Z)
    (Set.range (ι := ↥(pullback f g))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(pullback f g).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (pullback.snd f g))) ≫
              g.base)) :
        (a : ↥(pullback f g)) → ↥Z))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₂ :
  Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) (Function.comp (β := ↥Y) ⇑g ⇑(pullback.snd f g)))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₃ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₄ :
  Eq (α := Set ↥Z) (⇑g '' (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)) (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₅ :
  Eq (α := Set ↥Z) (⇑g '' (↑{ carrier := ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ : Opens ↥Y } : Set ↥Y))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g ≫ f))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
have rw₆ : Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier))
  (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
Tactic: rw [pullback.condition, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
    range_pullbackSnd, Opens.map_obj, Opens.coe_mk,
    Set.image_preimage_eq_inter_range, 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 f g)) ⇑(pullback.snd f g ≫ g))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₁ :
  Eq (α := Set ↥Z)
    (Set.range (ι := ↥(pullback f g))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(pullback f g).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (pullback.snd f g))) ≫
              g.base)) :
        (a : ↥(pullback f g)) → ↥Z))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₂ :
  Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) (Function.comp (β := ↥Y) ⇑g ⇑(pullback.snd f g)))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₃ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₄ :
  Eq (α := Set ↥Z) (⇑g '' (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)) (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₅ :
  Eq (α := Set ↥Z) (⇑g '' (↑{ carrier := ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ : Opens ↥Y } : Set ↥Y))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₆ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g ≫ f))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
have rw₇ : (Scheme.Hom.opensRange f).carrier ∩ Set.range (ι := ↥Y) ⇑g = Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g
Tactic: rw [pullback.condition, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
    range_pullbackSnd, Opens.map_obj, Opens.coe_mk,
    Set.image_preimage_eq_inter_range, 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 f g)) ⇑(pullback.snd f g ≫ g))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₁ :
  Eq (α := Set ↥Z)
    (Set.range (ι := ↥(pullback f g))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(pullback f g).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (pullback.snd f g))) ≫
              g.base)) :
        (a : ↥(pullback f g)) → ↥Z))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₂ :
  Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) (Function.comp (β := ↥Y) ⇑g ⇑(pullback.snd f g)))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₃ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₄ :
  Eq (α := Set ↥Z) (⇑g '' (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)) (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₅ :
  Eq (α := Set ↥Z) (⇑g '' (↑{ carrier := ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ : Opens ↥Y } : Set ↥Y))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₆ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₇ : (Scheme.Hom.opensRange f).carrier ∩ Set.range (ι := ↥Y) ⇑g = Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g ≫ f))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
have rw₈ : (↑(Scheme.Hom.opensRange f) : Set ↥Z) ∩ Set.range (ι := ↥Y) ⇑g = Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g
Tactic: rw [pullback.condition, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
    range_pullbackSnd, Opens.map_obj, Opens.coe_mk,
    Set.image_preimage_eq_inter_range, 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 f g)) ⇑(pullback.snd f g ≫ g))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₁ :
  Eq (α := Set ↥Z)
    (Set.range (ι := ↥(pullback f g))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(pullback f g).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (pullback.snd f g))) ≫
              g.base)) :
        (a : ↥(pullback f g)) → ↥Z))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₂ :
  Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) (Function.comp (β := ↥Y) ⇑g ⇑(pullback.snd f g)))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₃ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₄ :
  Eq (α := Set ↥Z) (⇑g '' (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)) (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₅ :
  Eq (α := Set ↥Z) (⇑g '' (↑{ carrier := ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ : Opens ↥Y } : Set ↥Y))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₆ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₇ : (Scheme.Hom.opensRange f).carrier ∩ Set.range (ι := ↥Y) ⇑g = Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g
rw₈ : (↑(Scheme.Hom.opensRange f) : Set ↥Z) ∩ Set.range (ι := ↥Y) ⇑g = Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g ≫ f))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
have rw₉ : Eq (α := Set ↥Z) (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g) (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
Tactic: rw [pullback.condition, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
    range_pullbackSnd, Opens.map_obj, Opens.coe_mk,
    Set.image_preimage_eq_inter_range, 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
⊢ 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 (ι := ↥(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)
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)
⊢ 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 (ι := ↥(pullback g f)) (Function.comp (β := ↥Y) ⇑g ⇑(pullback.fst g 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 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)
⊢ 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.image (α := ↥Y) (⇑g) (Set.range (ι := ↥(pullback g f)) ⇑(pullback.fst g 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 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)
⊢ 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) (⇑g '' (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)) (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)
⊢ 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) (⇑g '' (↑{ carrier := ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier, is_open' := sorry : Opens ↥Y } : Set ↥Y))
  (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)
⊢ 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.image (α := ↥Y) (⇑g) (⇑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)
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback g f)) ⇑(pullback.fst g f ≫ g))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
have rw₆ : (Scheme.Hom.opensRange f).carrier ∩ Set.range (ι := ↥Y) ⇑g = 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]