awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x : forget.obj X × forget.obj Y).1
h2 : (pullback.snd f g) z = (↑x : forget.obj X × forget.obj Y).2
⊢ (↑(Function.comp (β := (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g)))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom) :
              (a : (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g))) →
                (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g)))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) →
                (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g)))
            z) :
        forget.obj X × forget.obj Y).1 =
    (↑x : forget.obj X × forget.obj Y).1
have h : (ConcreteCategory.hom (FC := TypeCat.Fun) (pullback.fst (forget.map f) (forget.map g)) :
      (a : pullback (forget.map f) (forget.map g)) → forget.obj X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g) :
          (a : forget.obj (pullback f g)) → pullback (forget.map f) (forget.map g))
        z :
      pullback (forget.map f) (forget.map g)) =
  (↑x : forget.obj X × forget.obj Y).1
Tactic: simp only [Function.comp_apply, Types.pullbackIsoPullback_hom_fst]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x : forget.obj X × forget.obj Y).1
h2 : (pullback.snd f g) z = (↑x : forget.obj X × forget.obj Y).2
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (pullback.fst (forget.map f) (forget.map g)) :
        (a : pullback (forget.map f) (forget.map g)) → forget.obj X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g) :
            (a : forget.obj (pullback f g)) → pullback (forget.map f) (forget.map g))
          z :
        pullback (forget.map f) (forget.map g)) =
    (↑x : forget.obj X × forget.obj Y).1
have h : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := pullback (forget.map f) (forget.map g)) (pullbackComparison forget f g)
          (pullback.fst (forget.map f) (forget.map g))) :
      (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) → (fun (X : Type u) ↦ X) (forget.obj X))
    z =
  (↑x : forget.obj X × forget.obj Y).1
Tactic: rwa [← types_comp_apply (g := pullback.fst _ _), pullbackComparison_comp_fst]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x : forget.obj X × forget.obj Y).1
h2 : (pullback.snd f g) z = (↑x : forget.obj X × forget.obj Y).2
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := pullback (forget.map f) (forget.map g)) (pullbackComparison forget f g)
            (pullback.fst (forget.map f) (forget.map g))) :
        (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) → (fun (X : Type u) ↦ X) (forget.obj X))
      z =
    (↑x : forget.obj X × forget.obj Y).1
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (pullback.fst (forget.map f) (forget.map g)) :
        (a : pullback (forget.map f) (forget.map g)) → forget.obj X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g) :
            (a : forget.obj (pullback f g)) → pullback (forget.map f) (forget.map g))
          z :
        pullback (forget.map f) (forget.map g)) =
    (↑x : forget.obj X × forget.obj Y).1
have h₁ : (ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (pullback.fst f g)) :
      (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) → (fun (X : Type u) ↦ X) (forget.obj X))
    z =
  (↑x : forget.obj X × forget.obj Y).1
Tactic: rwa [← types_comp_apply (g := pullback.fst _ _), pullbackComparison_comp_fst]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x : forget.obj X × forget.obj Y).1
h2 : (pullback.snd f g) z = (↑x : forget.obj X × forget.obj Y).2
⊢ (↑(Function.comp (β := (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g)))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom) :
              (a : (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g))) →
                (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g)))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) →
                (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g)))
            z) :
        forget.obj X × forget.obj Y).2 =
    (↑x : forget.obj X × forget.obj Y).2
have h : (ConcreteCategory.hom (FC := TypeCat.Fun) (pullback.snd (forget.map f) (forget.map g)) :
      (a : pullback (forget.map f) (forget.map g)) → forget.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g) :
          (a : forget.obj (pullback f g)) → pullback (forget.map f) (forget.map g))
        z :
      pullback (forget.map f) (forget.map g)) =
  (↑x : forget.obj X × forget.obj Y).2
Tactic: simp only [Function.comp_apply, Types.pullbackIsoPullback_hom_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x : forget.obj X × forget.obj Y).1
h2 : (pullback.snd f g) z = (↑x : forget.obj X × forget.obj Y).2
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (pullback.snd (forget.map f) (forget.map g)) :
        (a : pullback (forget.map f) (forget.map g)) → forget.obj Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g) :
            (a : forget.obj (pullback f g)) → pullback (forget.map f) (forget.map g))
          z :
        pullback (forget.map f) (forget.map g)) =
    (↑x : forget.obj X × forget.obj Y).2
have h : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := pullback (forget.map f) (forget.map g)) (pullbackComparison forget f g)
          (pullback.snd (forget.map f) (forget.map g))) :
      (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) → (fun (X : Type u) ↦ X) (forget.obj Y))
    z =
  (↑x : forget.obj X × forget.obj Y).2
Tactic: rwa [← types_comp_apply (g := pullback.snd _ _), pullbackComparison_comp_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x : forget.obj X × forget.obj Y).1
h2 : (pullback.snd f g) z = (↑x : forget.obj X × forget.obj Y).2
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := pullback (forget.map f) (forget.map g)) (pullbackComparison forget f g)
            (pullback.snd (forget.map f) (forget.map g))) :
        (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) → (fun (X : Type u) ↦ X) (forget.obj Y))
      z =
    (↑x : forget.obj X × forget.obj Y).2
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (pullback.snd (forget.map f) (forget.map g)) :
        (a : pullback (forget.map f) (forget.map g)) → forget.obj Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g) :
            (a : forget.obj (pullback f g)) → pullback (forget.map f) (forget.map g))
          z :
        pullback (forget.map f) (forget.map g)) =
    (↑x : forget.obj X × forget.obj Y).2
have h₁ : (ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (pullback.snd f g)) :
      (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) → (fun (X : Type u) ↦ X) (forget.obj Y))
    z =
  (↑x : forget.obj X × forget.obj Y).2
Tactic: rwa [← types_comp_apply (g := pullback.snd _ _), pullbackComparison_comp_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Epi (X := forgetToTop.obj (pullback f g)) (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
    (pullbackComparison forgetToTop f g)
have refine : Epi (X :=
  Functor.obj
    (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
      TopCat.carrier))
    (forgetToTop.obj (pullback f g)))
  (Y :=
  Functor.obj
    (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
      TopCat.carrier))
    (pullback (forgetToTop.map f) (forgetToTop.map g)))
  (CategoryTheory.Functor.map
    (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
      TopCat.carrier))
    (pullbackComparison forgetToTop f g))
Tactic: refine (CategoryTheory.forget TopCat).epi_of_epi_map ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Epi (X :=
    Functor.obj
      (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
        TopCat.carrier))
      (forgetToTop.obj (pullback f g)))
    (Y :=
    Functor.obj
      (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
        TopCat.carrier))
      (pullback (forgetToTop.map f) (forgetToTop.map g)))
    (CategoryTheory.Functor.map
      (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
        TopCat.carrier))
      (pullbackComparison forgetToTop f g))
have rw : Function.Surjective (α :=
  (fun (X : Type u) ↦ X)
    (Functor.obj
      (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
        TopCat.carrier))
      (forgetToTop.obj (pullback f g))))
  (β :=
  (fun (X : Type u) ↦ X)
    (pullback (X :=
      Functor.obj
        (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
          TopCat.carrier))
        (forgetToTop.obj X))
      (CategoryTheory.Functor.map
        (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
          TopCat.carrier))
        (forgetToTop.map f))
      (CategoryTheory.Functor.map
        (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
          TopCat.carrier))
        (forgetToTop.map g))))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
        (pullbackComparison
          (forgetToTop ⋙
            CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
              TopCat.carrier))
          f g)) :
    (a : (fun (X : Type u) ↦ X) ((CategoryTheory.forget TopCat).obj (forgetToTop.obj (pullback f g)))) →
      (fun (X : Type u) ↦ X)
        (pullback ((CategoryTheory.forget TopCat).map (forgetToTop.map f))
          ((CategoryTheory.forget TopCat).map (forgetToTop.map g))))
Tactic: rw [← CategoryTheory.epi_comp_iff_of_isIso _
    (pullbackComparison (CategoryTheory.forget TopCat) (forgetToTop.map f) (forgetToTop.map g)),
    ← _root_.CategoryTheory.Limits.pullbackComparison_comp, epi_iff_surjective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
x : ↥X
y : ↥Y
hxy : Eq (α := ↥Z) (f x : ↥Z) (g y : ↥Z)
e : P ≅ pullback f g := h.isoPullback
⊢ ∃ (p : ↥P), fst p = x ∧ snd p = y
have obtain : ∀ (z : ↥(pullback f g)) (hzl : (pullback.fst f g) z = x) (hzr : (pullback.snd f g) z = y),
  ∃ (p : ↥P), fst p = x ∧ snd p = y
Tactic: obtain ⟨z, hzl, hzr⟩ := AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback x y hxy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
x : ↥X
y : ↥Y
hxy : Eq (α := ↥Z) (f x : ↥Z) (g y : ↥Z)
e : P ≅ pullback f g := h.isoPullback
z : ↥(pullback f g)
hzl : (pullback.fst f g) z = x
hzr : (pullback.snd f g) z = y
⊢ ∃ (p : ↥P), fst p = x ∧ snd p = y
have h₁ : fst ((Iso.inv h.isoPullback) z : ↥P) = x ∧ snd ((Iso.inv h.isoPullback) z : ↥P) = y
Tactic: use h.isoPullback.inv.base z
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
⊢ Eq (α := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) (Set.preimage (β := ↥Z) (⇑g) (⇑f '' s))
have refine_1 : Subset (α := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) (Set.preimage (β := ↥Z) (⇑g) (⇑f '' s))
Tactic: refine subset_antisymm ?_ (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
refine_1 : Subset (α := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) (Set.preimage (β := ↥Z) (⇑g) (⇑f '' s))
⊢ Eq (α := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) (Set.preimage (β := ↥Z) (⇑g) (⇑f '' s))
have refine_2 : ∀ (x : ↥Y) (hx : Membership.mem (γ := Set ↥Y) (Set.preimage (β := ↥Z) (⇑g) (⇑f '' s)) x),
  Membership.mem (γ := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) x
Tactic: refine subset_antisymm ?_ (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
⊢ Subset (α := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) (Set.preimage (β := ↥Z) (⇑g) (⇑f '' s))
have refine_1 : Subset (α := Set ↥P) (⇑fst ⁻¹' s) (Set.preimage (β := ↥Z) (⇑(fst ≫ f)) (⇑f '' s))
Tactic: rw [Set.image_subset_iff, ← Set.preimage_comp, ← TopCat.coe_comp, ← Hom.comp_base, ← h.1.1]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
⊢ Subset (α := Set ↥P) (⇑fst ⁻¹' s) (Set.preimage (β := ↥Z) (⇑(fst ≫ f)) (⇑f '' s))
have refine_1 : Subset (α := Set ↥Z) (Set.image (α := ↥X) (⇑f) (Set.image (α := ↥P) (⇑fst) (⇑fst ⁻¹' s))) (⇑f '' s)
Tactic: rw [Hom.comp_base, TopCat.coe_comp, ← Set.image_subset_iff, Set.image_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
x : ↥Y
hx : Membership.mem (γ := Set ↥Y) (Set.preimage (β := ↥Z) (⇑g) (⇑f '' s)) x
⊢ Membership.mem (γ := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) x
have refine_2 : ∀ (y : ↥X) (hy : y ∈ s) (heq : Eq (α := ↥Z) (f y : ↥Z) (g x : ↥Z)),
  Membership.mem (γ := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) x
Tactic: obtain ⟨y, hy, heq⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
x : ↥Y
y : ↥X
hy : y ∈ s
heq : Eq (α := ↥Z) (f y : ↥Z) (g x : ↥Z)
⊢ Membership.mem (γ := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) x
have refine_2 : ∀ (o : ↥P) (hl : fst o = y) (hr : snd o = x), Membership.mem (γ := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) x
Tactic: obtain ⟨o, hl, hr⟩ := exists_preimage_of_isPullback h y x heq
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
x : ↥Y
y : ↥X
hy : y ∈ s
heq : Eq (α := ↥Z) (f y : ↥Z) (g x : ↥Z)
o : ↥P
hl : fst o = y
hr : snd o = x
⊢ Membership.mem (γ := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) x
have h₁ : Membership.mem (γ := Set ↥P) (⇑fst ⁻¹' s) o ∧ snd o = x
Tactic: use o
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
⊢ MorphismProperty.IsStableUnderBaseChange @Surjective
have refine : ∀ (X Y S : Scheme.{u_1}) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
  Surjective g → Surjective (X := pullback f g) (pullback.fst f g)
Tactic: refine .mk' ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : HasPullback f g
hg : Surjective g
⊢ Surjective (X := pullback f g) (pullback.fst f g)
have simp : ∀ (hg : Eq (α := Set ↥S) (Set.range (ι := ↥Y) ⇑g) Set.univ),
  Eq (α := Set ↥X) (Set.preimage (β := ↥S) (⇑f) (Set.range (ι := ↥Y) ⇑g)) Set.univ
Tactic: simp only [surjective_iff, ← Set.range_eq_univ, Scheme.Pullback.range_fst] at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : HasPullback f g
hg : Eq (α := Set ↥S) (Set.range (ι := ↥Y) ⇑g) Set.univ
⊢ Eq (α := Set ↥X) (Set.preimage (β := ↥S) (⇑f) (Set.range (ι := ↥Y) ⇑g)) Set.univ
have rw : Eq (α := Set ↥X) (Set.preimage (β := ↥S) (⇑f) Set.univ) Set.univ
Tactic: rw [hg, Set.preimage_univ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : HasPullback f g
hg : Eq (α := Set ↥S) (Set.range (ι := ↥Y) ⇑g) Set.univ
rw : Eq (α := Set ↥X) (Set.preimage (β := ↥S) (⇑f) Set.univ) Set.univ
⊢ Eq (α := Set ↥X) (Set.preimage (β := ↥S) (⇑f) (Set.range (ι := ↥Y) ⇑g)) Set.univ
have rw₁ : Eq.{u_1 + 1} (α := Set ↥X) Set.univ Set.univ
Tactic: rw [hg, Set.preimage_univ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (hypothesis)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
⊢ v 𝒰 f g i j ⟶ v 𝒰 f g j i
have this : HasPullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
Tactic: have : HasPullback (pullback.snd _ _ ≫ 𝒰.f i ≫ f) g :=
    hasPullback_assoc_symm (𝒰.f j) (𝒰.f i) (𝒰.f i ≫ f) g
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (hypothesis)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this : HasPullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
⊢ v 𝒰 f g i j ⟶ v 𝒰 f g j i
have this₁ : HasPullback (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
Tactic: have : HasPullback (pullback.snd _ _ ≫ 𝒰.f j ≫ f) g :=
    hasPullback_assoc_symm (𝒰.f i) (𝒰.f j) (𝒰.f j ≫ f) g
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this_1 : HasPullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ v 𝒰 f g i j ⟶ v 𝒰 f g j i
have refine : pullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g ⟶ v 𝒰 f g j i
Tactic: refine (pullbackSymmetry ..).hom ≫ (pullbackAssoc ..).inv ≫ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this_1 : HasPullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ pullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g ⟶ v 𝒰 f g j i
have refine : pullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g ⟶
  pullback (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
Tactic: refine ?_ ≫ (pullbackAssoc ..).hom ≫ (pullbackSymmetry ..).hom
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this_1 : HasPullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ pullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g ⟶
    pullback (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
have refine_1 : Eq (α := pullback (𝒰.f j) (𝒰.f i) ⟶ Z) ((pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) ≫ 𝟙 Z)
  (Iso.hom (pullbackSymmetry (𝒰.f j) (𝒰.f i)) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f)
Tactic: refine pullback.map _ _ _ _ (pullbackSymmetry _ _).hom (𝟙 _) (𝟙 _) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this_1 : HasPullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
refine_1 :
  Eq (α := pullback (𝒰.f j) (𝒰.f i) ⟶ Z) ((pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) ≫ 𝟙 Z)
    (Iso.hom (pullbackSymmetry (𝒰.f j) (𝒰.f i)) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f)
⊢ pullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g ⟶
    pullback (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
have refine_2 : g ≫ 𝟙 Z = 𝟙 Y ≫ g
Tactic: refine pullback.map _ _ _ _ (pullbackSymmetry _ _).hom (𝟙 _) (𝟙 _) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this_1 : HasPullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ Eq (α := pullback (𝒰.f j) (𝒰.f i) ⟶ Z) ((pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) ≫ 𝟙 Z)
    (Iso.hom (pullbackSymmetry (𝒰.f j) (𝒰.f i)) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f)
have refine_1 : Eq (α := pullback (𝒰.f j) (𝒰.f i) ⟶ Z) ((pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) ≫ 𝟙 Z)
  (pullback.fst (𝒰.f j) (𝒰.f i) ≫ 𝒰.f j ≫ f)
Tactic: rw [pullbackSymmetry_hom_comp_snd_assoc, pullback.condition_assoc, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this_1 : HasPullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
refine_1 :
  Eq (α := pullback (𝒰.f j) (𝒰.f i) ⟶ Z) ((pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) ≫ 𝟙 Z)
    (pullback.fst (𝒰.f j) (𝒰.f i) ≫ 𝒰.f j ≫ f)
⊢ Eq (α := pullback (𝒰.f j) (𝒰.f i) ⟶ Z) ((pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) ≫ 𝟙 Z)
    (Iso.hom (pullbackSymmetry (𝒰.f j) (𝒰.f i)) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f)
have refine_1₁ : Eq (α := pullback (𝒰.f j) (𝒰.f i) ⟶ Z) ((pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) ≫ 𝟙 Z)
  (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f)
Tactic: rw [pullbackSymmetry_hom_comp_snd_assoc, pullback.condition_assoc, Category.comp_id]